summaryrefslogtreecommitdiff
path: root/src/gen_lib/prompt.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-09Support short-circuiting of Boolean expressions in LemThomas Bauereiss
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-05Add support for undefined bit oracle to Lem shallow embeddingThomas 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-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-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
2017-10-31Pretty-print Sail assertions in LemThomas Bauereiss
2017-10-19Make some potentially non-terminating library functions terminateThomas Bauereiss
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-27Add while-loops to Lem backendThomas Bauereiss
2017-08-24Begin refactoring Sail libraryThomas Bauereiss
2017-08-08Glue together Sail prelude and Lem libraryThomas Bauereiss
2017-06-21Pretty-print bitvector expressionsThomas Bauereiss
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-03-23the interpreter/shallow expects little-endian memory-valuesShaked Flur
2016-12-09sail changes for making lem embedding Isabelle-friendlierChristopher Pulte
2016-11-27make outcome_s contain the instruction state pretty print rather than the ins...Christopher Pulte
2016-11-14add option -lem_sequential for producing shallow embedding that refers to sta...Christopher Pulte
2016-11-08fixesChristopher Pulte
2016-11-07factor out regfp analysis types into etc/regfp.sailChristopher Pulte
2016-10-28shallow embedding progressChristopher Pulte
2016-10-27more shallow embedding fixesChristopher Pulte
2016-10-21shallow embedding progressChristopher Pulte
2016-10-10changed the way registers/register fields work, fixes, nicer names for new le...Christopher Pulte
2016-10-06move type definitions that both interpreter and shallow embedding use to sail...Christopher Pulte
2016-09-30fixes, update isntruction_analysis for NIAs and DIAChristopher Pulte
2016-09-25nicer lem output: no more unecessary 'unit' returns if if-expressions, for-lo...Christopher Pulte
2016-09-23sail-to-lem progressChristopher Pulte
2016-09-21fixesChristopher Pulte
2016-09-19sail-to-lem progressChristopher Pulte
2016-09-07push some lem pp changesChristopher Pulte
2015-12-21fixes, pp progressChristopher
2015-12-15better location informationChristopher
2015-12-03added prompt.lem for connecting to concurrency model and {power,armv8}_extras...Christopher Pulte
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 05:09:29 +0000