summaryrefslogtreecommitdiff
path: root/src/gen_lib
AgeCommit message (Expand)Author
2020-04-10Add Lem builtins for operations on realsThomas Bauereiss
2020-04-10Implement hex_str for LemThomas Bauereiss
2019-11-07Fix Jenkins buildAlasdair Armstrong
2019-11-07Backport fixes to SMT generation from poly_mapping branchAlasdair Armstrong
2019-08-14Inline reg_deref in Lem outputThomas Bauereiss
2019-07-31Revert "Need to separate out the 0.10 lem library from upcoming 0.11"Alasdair Armstrong
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair Armstrong
2019-07-18Support DMB/DSB domainsShaked Flur
2019-06-18Implement count_leading_zeros in LemThomas Bauereiss
2019-06-06Fix tdiv_int and tmod_int bindings for LemThomas Bauereiss
2019-04-25More read/write function updatesBrian Campbell
2019-04-25lem gen_lib: update read/write functions to take (dummy) addrsize argument as...Jon French
2019-03-15Lem: Add missing implementations of vector_truncateLSBThomas Bauereiss
2019-02-04Add dec_str builtin to lemAlasdair Armstrong
2019-02-04Test lem output by running end-to-end tests using ocaml via lemAlasdair Armstrong
2019-01-09Merge sail2 into monadsThomas Bauereiss
2019-01-04Add a few helper lemmasThomas Bauereiss
2018-12-23Remove a comment that breaks Isabelle buildThomas Bauereiss
2018-12-18Merge branch 'sail2' into monadsThomas Bauereiss
2018-12-03Add Write_mem event/outcome without tagThomas Bauereiss
2018-12-03Make names of memory r/w events more consistentThomas Bauereiss
2018-11-30Rename Undefined outcome to ChooseThomas Bauereiss
2018-11-29Add separate outcome/event for tagged memory loadsThomas Bauereiss
2018-11-29Add some helper lemmas to Isabelle libThomas Bauereiss
2018-11-20Use nat instead of (list bitU) for addresses in monad outcomesThomas Bauereiss
2018-10-31Add helper functions in Sail Lem libraryThomas Bauereiss
2018-10-31Monad refactoring in Lem shallow embeddingThomas Bauereiss
2018-10-16Re-implement space-related mapping functions in Sail rather than backendsJon French
2018-09-19separate decimal_string_of_bits from string_of_bitsJon French
2018-09-19src/gen_lib/sail2_string.lem: more Lem monomorphisations for hex_bits_N_match...Jon French
2018-07-12Minor fix to support OCaml 4.02.3Shaked Flur
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
2018-07-11Fix some signedness bugsThomas Bauereiss
2018-07-10disable printing when compiling to Lem to keep rmem happyJon French
2018-07-10Aarch64 mono script updateBrian Campbell
2018-07-09Simplify treating of undefined_bool in Lem libraryThomas Bauereiss
2018-06-25Support bitlist representation in Sail2_stringThomas Bauereiss
2018-06-21Follow Sail2 renaming in Isabelle libraryThomas Bauereiss
2018-06-21changes to riscv model to support rmemJon French
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-06-11Merge branch 'sail2' into mappingsJon French
2018-05-31Fixes to get ARM u-boot working in Sail.Alasdair Armstrong
2018-05-23riscv decode now uses mapping-decode and passes testsJon French
2018-05-21further RISCV mapping: all extant non-compressed instructions doneJon French
2018-05-18more riscv mappings; riscv now builds successfully to lem which builds to isa...Jon French
2018-05-17Use an intermediate base_monad type alias in Lem,Brian Campbell
2018-05-16Declare hol automatic termination in sail_valuesRamana Kumar
2018-05-11Add Boolean short-circuiting to state monadThomas Bauereiss
2018-05-11Merge branch 'sail2' into cheri-monoThomas Bauereiss
2018-05-11Remove buggy bit list comparison functions from Lem libraryThomas Bauereiss