summaryrefslogtreecommitdiff
path: root/src/rewrites.ml
AgeCommit message (Expand)Author
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-28Merge branch 'sail2' into rmem_interpreterJon French
2018-12-27refactor val-spec AST to store externs as an assoc-list rather than a functio...Jon French
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
2018-10-22Coq: work around constructors with tupled argumentsBrian Campbell
2018-10-16rewrites: remove now-unnecessary temporary string hack from rewrite_defs_pat_...Jon French
2018-10-11Change the function type in the ASTAlasdair
2018-10-04rename stringappend ids for more readable generated codeJon French
2018-10-01Extend Coq pattern match completeness rewrite to let patternsBrian Campbell
2018-10-01New rewriting pass toplevel_string_appendJon French
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-19rewrite_defs_pat_string_append: fix bug with guarded SomeJon French
2018-09-17Rewrites.rewrite_defs_mapping_patterns: emit an explicit type annotation on t...Jon French
2018-09-13C: Fix an issue with assigning to unitialized variables at end of blocksAlasdair Armstrong
2018-09-12Jenkins: Fix deprecation warningsAlasdair Armstrong
2018-09-04Add a rewrite to minimise the number of functions marked as recursiveBrian Campbell
2018-08-31rewrite_defs_pat_string_append: only guard the innermost recursive pattern, a...Jon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:39:30 +0000