summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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-09-02Consider case expressions in early return rewriteThomas Bauereiss
2020-08-27Perform truncation of hex literals for C backend (really for isla)Brian Campbell
2020-08-07Allow C/IR builds to use mono_rewrites without the rest of monomorphisationBrian Campbell
2020-05-22Fix atomicity of register field writesAlasdair
2020-05-21Merge branch 'sail2' into mono-tweaksAlasdair
2020-05-15Add coverage tracking toolAlasdair
2020-05-11Functorise and refactor C code generatorAlasdair
2020-04-21Mono: Check for non-constant calls to make_the_valueThomas Bauereiss
2020-04-21Add rewrite for constant-folding top-level letbindingsThomas Bauereiss
2020-04-21Consider literals in pattern disjointness checkThomas Bauereiss
2020-04-21Handle more cases in bitvector cast rewriteThomas Bauereiss
2020-04-21Tweak types of loop combinators for prover combinatorsThomas Bauereiss
2020-04-21Rewrite vector concat lexps to sequences of assignmentsThomas Bauereiss
2020-04-21Be more careful about type annotations in rewrites to LemThomas Bauereiss
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:28 +0000