summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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-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
2019-01-14Make rewriting of foreach loops for Lem more robustThomas Bauereiss
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
2019-01-08Improvements for v85Alasdair Armstrong
2019-01-02Coq: tweak recently introduced type check to ignore effectsBrian Campbell
2018-12-31Last rewrite reordering needs more typecheckingBrian Campbell
2018-12-31Coq: move function clause merging to keep measure argument intactBrian Campbell
2018-12-30Sort dependencies of termination measures properlyBrian Campbell
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-26More cleanupAlasdair Armstrong
2018-12-26Some cleanupAlasdair Armstrong
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-21Expand synonyms in generated mapping val-specsAlasdair Armstrong
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
2018-12-18Fix rewriter issuesAlasdair Armstrong
2018-12-18Store function instantiation information within annotations, so we don'tAlasdair
2018-12-13Merge remote-tracking branch 'origin/sail2' into asl_flowAlasdair
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
2018-12-12Add a test case for various simple boolean propertiesAlasdair Armstrong
2018-12-12Generalise existentials for non-integer type variablesAlasdair
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
2018-12-10Various changes:Alasdair Armstrong
2018-12-08Compiling againAlasdair
2018-12-07Working on better flow typing for ASLAlasdair Armstrong
2018-12-06Re-factor initial checkAlasdair Armstrong
2018-12-04Remove FES_Fexps constructorAlasdair Armstrong
2018-12-04Simplify kinds in the ASTAlasdair Armstrong
2018-11-19Don't re-check AST repeatedly in exp_lift_assign re-writeAlasdair Armstrong
2018-11-19Ensure sizeof re-writing occurs for configuration registersAlasdair Armstrong
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-10-31Add rewriting pass for not-patternsAlasdair Armstrong
2018-10-31Rename Reporting_basic to ReportingAlasdair Armstrong
2018-10-31Improve error messages for unsolved function quantifiersAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:33:59 +0000