summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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 some more test casesAlasdair Armstrong
2019-01-22Add a pragma for unrolling recursive functionsAlasdair Armstrong
2019-01-22Bump opam version for release.Robert Norton
2019-01-22Build isabelle and hol files in lib from lem before opam install.Robert Norton
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
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-21The RISCV environment variable collides with common usage by the RISC-V toolc...Prashanth Mundkur
2019-01-21Pass Lem library path to IsabelleThomas Bauereiss
2019-01-21Don't require manual set up of Isabelle session directoriesThomas Bauereiss
2019-01-21Fix typo in install instructionsAlasdair Armstrong
2019-01-21Remove old emacs mode to avoid confusionAlasdair Armstrong
2019-01-21Update manual snapshot and add basic sail -latex documentationAlasdair Armstrong
2019-01-21Fix build of Isabelle documentationThomas Bauereiss
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-19wibShaked Flur
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-13update READMEPeter Sewell
2019-01-13update README with current model reposPeter Sewell
2019-01-11Updates for sail-arm releaseAlasdair Armstrong
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
2019-01-09Update Coq snapshotsBrian Campbell
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-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2019-01-08Improvements for v85Alasdair Armstrong
2019-01-04Add a few helper lemmasThomas Bauereiss
2019-01-04C library: fix fprintf warnings in lib/elf.cAlastair Reid
2019-01-04Arm ElfMain: fix minor type errorsAlastair Reid
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-01Coq: update instr_kinds from LemBrian 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-29Coq: ensure that recursive functions computeBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 07:02:57 +0000