- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.
Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
* commit '8d4a8eb238090999b4b41f588d5fa63453d58ae8':
SELFOUR-421: fix coding style
SELFOUR-421: fix drefine
SELFOUR-421: add device bit in UntypedCap and FrameCap in capdl
SELFOUR-421: infoflow and infoflow_c builds
SELFOUR-421: crefine builds
SELFOUR-421: commit before change abstract again
SELFOUR-421: fix refine
SELFOUR-421: a defend version before wild changes
SELFOUR-421: new haskell spec after UserDataDevice changes
SELFOUR-421: broken crefine after conversation with gerwin
SELFOUR-421: up to VSpace_C done
SELFOUR-421: temp work in CSpace_C
SELFOUR-421: fixed Refine after merge with master
SELFOUR-421: retranslate haskell after merge with master
SELFOUR-421: random uncommitted stuff before merge
SELFOUR-421: retranslate haskell for fixed range check
SELFOUR-421: refine done
SELFOUR-421: added check to decoding asid control invocations and stole an asid bit from the high bits not the low ones
SELFOUR-421: AInvs done, no added invariants yet
SELFOUR-421: first attempt at abstract spec
Architecture names follow L4V_ARCH-style naming conventions ('ARM', 'FAKE64').
However, the standalone parser does not make use of the L4V_ARCH environment
variable.
The standalone-parser Makefile builds all architectures at once, producing
binaries at 'ARM/c-parser', 'FAKE64/c-parser', and similarly for the tokenizer.
There are also wrapper scripts 'c-parser' and 'tokenizer' in the
standalone-parser directory, which take an architecture on the command line.
The make_munge.sh script calls the appropriate binary parser directly.
Gerwin Klein
Joel Beeren
Rafal Kolanski
Xin Gao
Matthew Brecknell
Matthew Brecknell
Alejandro Gomez-Londono