summaryrefslogtreecommitdiff
path: root/aarch64/aarch64_extras_embed_sequential.lem
AgeCommit message (Collapse)Author
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
- Update Lem bindings and extras files - Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's (used for cap_size in the CHERI spec) - Add Lem and Isabelle Makefile targets for CHERI
2018-01-31Add wrappers around Lem operators using bitvector type classThomas Bauereiss
Makes bitvector typeclass instance dictionaries disappear from generated Isabelle output.
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.