summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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-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-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-15Add a rewriting pass for constant propagation in mutrecsThomas Bauereiss
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-11Improve ocamldoc commentsAlasdair Armstrong
2019-03-08Rewriter: Cleanup old sizeof rewritesAlasdair Armstrong
2019-03-07Also remove impossible if-branchesThomas Bauereiss
2019-03-07Add a rewrite to remove impossible cases on integer literalsBrian Campbell
2019-03-04Fix aarch64_small test XML for jenkinsAlasdair Armstrong
2019-03-04Fix execute splitting to work when constructors have constraints.Alasdair Armstrong
2019-03-04Merge branch 'sail2' into rmem_interpreterJon French
2019-02-27Tweaks to C compilation to make it more usable for embedding into other programsAlasdair Armstrong
2019-02-25Merge branch 'sail2' into rmem_interpreterJon French
2019-02-21Allow monomorphisation with C generationAlasdair
2019-02-21Fix specialization bug involving function annotations not matching valspecsAlasdair
2019-02-18Make sure we remove bitvector patterns within guardsAlasdair Armstrong
2019-02-15Tweak intermediate language names for loop combinators to allow reparsingBrian Campbell
2019-02-14Don't do any rewrites when checking files for EmacsAlasdair Armstrong
2019-02-13Merge branch 'sail2' into rmem_interpreterJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:23:15 +0000