summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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
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
2019-02-08Add missing functions to HOL monad wrapperThomas Bauereiss
2019-02-08Rewrite type definitions in rewrite_nexp_idsThomas Bauereiss
2019-02-08Remove dead code from type-checkerAlasdair
2019-02-07Monomorphisation tweaks for v8.5Thomas Bauereiss
2019-02-06Fix some testsAlasdair Armstrong
2019-02-06Remove all sizeof rewriting from C compilationAlasdair
2019-02-05Use more general types for lexps in the internal lets rewriting passBrian Campbell
2019-02-03Merge branch 'sail2' into rmem_interpreterJon French
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Fix missing typedef cases in OCaml outputAlasdair
2019-01-31Turn on cast insertion for -lem_mwords and revert b826df25Brian Campbell
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Make recheck_defs_without_effects restore old flag properlyBrian Campbell
2019-01-23Make rewriting of E_assign a bit more robustThomas Bauereiss
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
2019-01-17Fix bug in letbind_effects rewriteThomas Bauereiss
2019-01-14Add a function to perform re-writes in parallelAlasdair
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:01:31 +0000