#
48b3a8b4 |
|
04-Oct-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
update object and field widths for x64, and remove some magic numbers In X64 update the following to match the C kernel: - TCB size-bits (11). - Endpoint size-bits (4). - Guard bits (58). - Message registers. For all architectures, replace magic numbers with defined constants in specifications, and as far as possible in proofs: - tcb_bits in abstract spec. - tcbBlockSizeBits, cteSizeBits, ntfnSizeBits, epSizeBits in Haskell spec, Haskell and C refinement proofs.
|