summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
2020-05-11Functorise and refactor C code generatorAlasdair
2020-04-14Add add_symbol to the API of Process_fileAlasdair
2020-01-22Preserve effect annotation when realising mappingsThomas Bauereiss
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
2020-01-17Merge scattered mapping fixesJames Clarke
2020-01-16Allow effects on mappingsAlasdair Armstrong
2019-12-03Prover backends: Expand Int type synonyms in type definitionsThomas Bauereiss
2019-11-29Merge branch 'word-numerals' into sail2Thomas Bauereiss
2019-11-26Allow overriding of generated mapping functionsThomas Bauereiss
2019-11-06Allow specifying specific fields of a register as constant with :fixed_regist...Alasdair Armstrong
2019-11-06Add toplevel commands to fix specific register values and simply spec accordi...Alasdair Armstrong
2019-08-13Coq: fix non-exhaustive pattern match failure in riscv duopodBrian Campbell
2019-08-02Fix all warnings (except for two lem warnings)Alasdair Armstrong
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-08-01Merge remote-tracking branch 'origin/rv_duopod_fix' into sail2Alasdair Armstrong
2019-07-16Fix all remaining tests for this branchAlasdair
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-07-11Make sure constant folding won't fold external definitions that also have sai...Alasdair Armstrong
2019-06-30Fix bug with toplevel pattern in RISC-V duopodAlasdair
2019-06-19Rewriting improvements for monomorphic aarch64_smallBrian Campbell
2019-06-18Fix handling of E_internal_plet in rewriteThomas Bauereiss
2019-06-13Fix some bugs in Lem rewriterThomas Bauereiss
2019-06-12Handle partial matches in guarded pattern rewriteThomas Bauereiss
2019-06-10Add well-formedness check for type schemes in valspecs.Brian Campbell
2019-06-06Add an option to pre-compile the axiomatic model for SMTAlasdair Armstrong
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-06-03Coq: support non-exhaustive pattern rewrite for exception handlingBrian Campbell
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-1594f445 introduced a new name for _ref_deref, add it to the effect rewritingBrian Campbell
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-20Fix: Reduce constant-fold time for ARM from 20min+ to 10sAlasdair Armstrong
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
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-13SMT: Add count_leading_zeros and more builtinsAlasdair
2019-04-11SMT: Add property and counterexample directiveAlasdair Armstrong
2019-04-10Coq: tweak measure rewrites slightlyBrian Campbell
2019-04-09SMT: Experimental Jib->SMT translationAlasdair Armstrong
2019-04-06Various bugfixes and improvementsAlasdair
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-03-27Interactive: Refactor sail.ml some moreAlasdair Armstrong
2019-03-27Interactive: Refactor sail.mlAlasdair Armstrong
2019-03-27Rewriter: Finish refactoring rewrite sequencesAlasdair Armstrong
2019-03-26Rewriter: Expose rewrite passes to interactive modeAlasdair Armstrong
2019-03-26Lem: Output constant bitvectors as hex or bin literalsThomas Bauereiss
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:50:11 +0000