summaryrefslogtreecommitdiff
path: root/src/gen_lib/state.lem
AgeCommit message (Expand)Author
2018-06-14rename all lem support files to sail2_foo to avoid conflict with sail1 in rmemJon French
2018-05-11Add Boolean short-circuiting to state monadThomas Bauereiss
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas 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-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-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-01-31Split base definitions of Lem monads and further built-ins (e.g. loop combina...Thomas Bauereiss
2018-01-29Add rreg effect to _reg_deref in fix_val_specs rewriteThomas Bauereiss
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Make some potentially non-terminating library functions terminateThomas Bauereiss
2017-10-02Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-29Support vector registers (other than bitvectors)Thomas Bauereiss
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
2017-09-28Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-27Add while-loops to Lem backendThomas Bauereiss
2017-09-21wibShaked Flur
2017-09-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-exper...Brian Campbell
2017-09-03added RISC-V strong-acquire/releaseShaked Flur
2017-09-02Remove dependency of state.lem on bitvector operationsThomas Bauereiss
2017-08-28Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-exper...Brian Campbell
2017-08-24Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-24Begin refactoring Sail libraryThomas Bauereiss
2017-08-23Update monomorphisation test scriptBrian Campbell
2017-08-22and fix that other placesChristopher Pulte
2017-08-22adapt state.lem to RISCV additionsChristopher Pulte
2017-08-17Add support for register types other than bitvector to state monadThomas Bauereiss
2017-08-15Improve and simplify handling of mutable local variablesThomas Bauereiss
2017-08-10Add support for early return to Lem backendThomas Bauereiss
2017-08-08Glue together Sail prelude and Lem libraryThomas Bauereiss
2017-06-21Pretty-print bitvector expressionsThomas Bauereiss
2017-06-02Add tag memory to Lem shallow embeddingThomas Bauereiss
2017-05-24fixed missing _tag bitsShaked Flur
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-03-23the interpreter/shallow expects little-endian memory-valuesShaked Flur
2016-11-15wrap state monad into list monoad for non-deterministic write exclusive opera...Christopher Pulte
2016-11-14add option -lem_sequential for producing shallow embedding that refers to sta...Christopher Pulte
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:50:43 +0000