summaryrefslogtreecommitdiff
path: root/src/gen_lib
AgeCommit message (Expand)Author
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
2018-05-09Fix printing of hex strings in LemThomas Bauereiss
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-09Run ARM built-in tests for Lem backend (via OCaml)Thomas Bauereiss
2018-05-09Support short-circuiting of Boolean expressions in LemThomas Bauereiss
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-04-20Have sign_extend in common Sail Lem library, use it and zero_extend inBrian Campbell
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
2018-04-18Move a few printing functions to sail_values.lemThomas Bauereiss
2018-04-18Move Lem shl_int, shr_int implementations from aarch64_extras to sail libBrian Campbell
2018-04-17Move some Lem library vector operations so that we also have mword versionsBrian Campbell
2018-04-05Cleanup repository by removing old and generated filesAlasdair Armstrong
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Machine words extract/update operations arguments are the other way aroundBrian Campbell
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
2018-03-05Add Print outcome to prompt monad for debugging and tracingThomas Bauereiss
2018-03-05Add support for undefined bit oracle to Lem shallow embeddingThomas Bauereiss
2018-03-02Use sail_lib.lem values in C backendAlasdair Armstrong
2018-02-27Get MIPS translated to LemThomas Bauereiss
2018-02-27Lem/OCaml compatibility fixesBrian Campbell
2018-02-26Rename some Isabelle theoriesThomas Bauereiss
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-22Some Lem/OCaml compatibility fixesBrian Campbell
2018-02-17Merge master branch into sail2 for OCaml 4.06 compatibilityThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 01:04:13 +0000