Domains are unnecessarily treated explicitly as 8-bit values within boot info.
Though there are existing proof constraints that limit the maximum domain value
to 8 bits, most of the code would permit domain values up to 32 bits. The
maximum value is unnecessarily constrained in boot info, a restriction which
this commit removes.
Closes VER-341
The XU3 uses a 5422 which for seL4's purposes is almost the same as
the Odroid XU's 5410. Define a new PLAT_EXYNOS54XX to cover both.
Keep PLAT_EXYNOS5410 and ...5422 for the few places (not in the
kernel) where the difference matters.
The c-parser can now parse these functions, but it does it by
discarding the inline ASM block, creating a misleading and likely
malformed function body. It is better to not translate these
with a DONT_TRANSLATE comment.
This change has been made for the current verification platform
only, and should probably be extended to any other verification
targets as necessary.
