summaryrefslogtreecommitdiff
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-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-02...without debug printingJon French
2019-01-02restore V_attempted_read behaviour after mergeJon French
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
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-27Coq: make solver try hints before stripping away existentialsBrian 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
2018-12-23Remove a comment that breaks Isabelle buildThomas Bauereiss
2018-12-22Added RISC-V fence.tsoShaked Flur
2018-12-22Improve error messages and debuggingAlasdair Armstrong
2018-12-21Simplify boolean existentialsAlasdair Armstrong
2018-12-21Expand synonyms in generated mapping val-specsAlasdair Armstrong
2018-12-20Make sure sail -v prints useful version infoAlasdair Armstrong
2018-12-20Fix monomorpisation tests with typechecker changesAlasdair Armstrong
2018-12-20RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ...Robert Norton
2018-12-19Improve sizeof rewriting performanceAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 14:35:11 +0000