summaryrefslogtreecommitdiff
path: root/src/pretty_print_lem.ml
AgeCommit message (Expand)Author
2020-11-25Fix Lem output for single element enumBrian Campbell
2020-09-29Refactor: Change AST type from a union to a structAlasdair
2020-09-28Refactor: Rename 'a defs to 'a astAlasdair
2020-09-28Move the ast defs wrapper into it's own fileAlasdair
2020-05-04Lem: Add some reserved identifiersThomas Bauereiss
2020-04-21Lem: Print more type annotationsThomas Bauereiss
2020-04-21Various monomorphisation fixesThomas Bauereiss
2020-04-21Handle more cases in bitvector cast rewriteThomas Bauereiss
2020-04-21Be more careful about type annotations in rewrites to LemThomas Bauereiss
2020-04-10Add Lem builtins for operations on realsThomas Bauereiss
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-05-21Lem: Fix bug in generation of val-specsThomas Bauereiss
2019-05-17Get all Lem tests working with separate bitvector typeAlasdair Armstrong
2019-05-17Experiment with making vector and bitvector distinct typesAlasdair Armstrong
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-13Merge branch 'sail2' into smt_experimentsAlasdair
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-13don't emit cache_op_kind enum in LemJon French
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-06Various bugfixes and improvementsAlasdair
2019-03-26Lem: Output constant bitvectors as hex or bin literalsThomas Bauereiss
2019-03-26Lem: Work around if-cascade indentation problemThomas Bauereiss
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13Tell Lem that records parametrised over Ints need the len typeclass annotationsBrian Campbell
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-19Refactor specializationAlasdair Armstrong
2019-02-18Rename Type_check.solve -> Type_check.solve_uniqueAlasdair Armstrong
2019-02-15Tweak intermediate language names for loop combinators to allow reparsingBrian Campbell
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
2019-02-08Add parameterization support for bitfields.Prashanth Mundkur
2019-02-05Ensure Lem output doesn't fail if there's a termination measure presentBrian Campbell
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-31Turn on cast insertion for -lem_mwords and revert b826df25Brian Campbell
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-28Lem: Be more careful about nexps occurring in the function signatureThomas Bauereiss
2019-01-17Work around an issue with type abbreviations in HOLThomas Bauereiss
2019-01-17Output configuration registers for LemThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:12:52 +0000