summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-23Add another flow-typing case for E_internal_pletThomas Bauereiss
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
2019-01-22Make sure there is an ocaml representation for optimized memory read forAlasdair
2019-01-22Make sure we optimize constrained union constructorsAlasdair
2019-01-21Update manual snapshot and add basic sail -latex documentationAlasdair Armstrong
2019-01-21Add output directory option for generated Isabelle auxiliary theoriesThomas Bauereiss
2019-01-21Fix some issues with latex generation so manual builds againAlasdair Armstrong
2019-01-21Fix a bug with type-checking and latex generationAlasdair Armstrong
2019-01-17Work around an issue with type abbreviations in HOLThomas Bauereiss
2019-01-17Output configuration registers for LemThomas Bauereiss
2019-01-17Fix bug in letbind_effects rewriteThomas Bauereiss
2019-01-16Latex: handle underscores when generating latex names.Prashanth Mundkur
2019-01-14Add options for output directories for the lem and coq backends.Prashanth Mundkur
2019-01-14Add a function to perform re-writes in parallelAlasdair
2019-01-14Support some more unification casesThomas Bauereiss
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-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Merge sail2 into monadsThomas Bauereiss
2019-01-09Coq: add parens around negative integer literalsBrian Campbell
2019-01-08Improvements for v85Alasdair Armstrong
2019-01-04Add a few helper lemmasThomas Bauereiss
2019-01-03Make sure to close file handles when printing error messagesAlasdair Armstrong
2019-01-03Comment out bisect coverage in ocamlbuild filesAlasdair Armstrong
2019-01-02Coq: tweak recently introduced type check to ignore effectsBrian Campbell
2019-01-02...without debug printingJon French
2019-01-02restore V_attempted_read behaviour after mergeJon French
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-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-28Remove opt_spc_matches_prefix from sail.h (fixes C tests)Jon French
2018-12-28Merge branch 'sail2' into rmem_interpreterJon French
2018-12-27Coq: avoid putting ambiguous numeric literals in Coq outputBrian Campbell
2018-12-27fix missed case in refactored val-spec extern parserJon French
2018-12-27Coq: fix name clashes and instantiation calculationBrian Campbell
2018-12-27new command line option -marshal <file> to marshal out rewritten AST to a fileJon French
2018-12-27remove unused previous-version-of-flow-typing functions from typecheckerJon French
2018-12-27basic Sail-side support for rmem use of interpreterJon French
2018-12-27refactor val-spec AST to store externs as an assoc-list rather than a functio...Jon French
2018-12-27pass typechecking environment around interpreter and rewritersJon French
2018-12-26More cleanupAlasdair Armstrong
2018-12-26Some cleanupAlasdair Armstrong
2018-12-26Add makefile target for building with Bisect coverageAlasdair Armstrong
2018-12-26More error messages improvmentsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 08:59:19 +0000