A C++ compiler will attempt to interpret 'return info' as an invocation of a copy
constructor. Even though the copy constructor is auto-generated (and eventually
completely eliminated due to inlining) and just does obvious member copying it
still results in an intermediate invocation that must take a reference to 'info'.
Because 'info' is a register variable it is not permissable to take a reference
to it. Manually reconstructing a new info from the .words keeps everything as
Plain Old Data

This branch does not have support for this platform.

zynq: Increase kernel window size (start at 0xe0000000) now that the elfloader does not attempt to access the serial port at 0xe0001000 after PD switch

Consolidating to one simulator to get simulator builds running again. The
source setup is still for multiple potential targets so it remains reasonably
easy to add different architectures like x86 to the Haskell model if needed.

HaskellCPU and Alpha implementations have fallen far behind the current
kernel structure, haven't been used for years, and are not included in
the build.

Removing them to avoid confusion.

separate benchmark output by tabs instead of spaces such that it is easier to paste into spreadsheet programs

Comparing a pointer against a literal without an explicit cast is not supported
by the C parser.

JIRA: VER-429

This has no effect on the code, but makes this value visible as a named
constant in Isabelle when importing C sources. It avoids us having to reference
120 as a magic number in numerous proofs.

This commit adds a two new output targets for the bitfield generator,
--autocorres-defs and --autocorres-proofs. These produce, respectively,
abstract definitions of the generated C functions suitable for use in
AutoCorres proofs and WP/simp lemmas suitable for use within AutoCorres proofs
of functions that call the generated C functions. Existing behaviour and
functionality should be unaffected.

Stdout is not suitable as an output target for these things.

Having the padding types as INT_MAX + 1 means C++ compilers will end up using
a signed 64 bit integer, as that is the only type that can have a value that
large, as well as the negative values our enums typically contain

The bitfield generator constructs tags as enums. The compiler is free to back
these by any type big enough to cover the enum. The generator emits code that
uses these tag values in mask and shift operations where the target type is
typically a uint32_t. As a result, it can produce code involving undefined
shifts like:

 (seL4_CapData_Badge & 0x1) << 31

This commit casts the tag value to the unsigned target type before masking to
ensure everything is done on an appropriate sized unsigned type.

JIRA: SELFOUR-193

The bitfield generator uses the macros CONST and PURE which, for libsel4, are
defined in macros.h.

trivial: Print domain values as unsigned integers in user errors.

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

With the comparison preceding this being done on unsigned integers, this avoids
confusing error messages like '-2147482648 >= 1'.