summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-01-13update READMEPeter Sewell
2019-01-13update README with current model reposPeter Sewell
2019-01-09Update Coq snapshotsBrian Campbell
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add parens around negative integer literalsBrian Campbell
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
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
2018-12-29Add separate termination_measure declarationsBrian Campbell
2018-12-27Coq: avoid putting ambiguous numeric literals in Coq outputBrian Campbell
2018-12-27Coq: fix name clashes and instantiation calculationBrian Campbell
2018-12-27Coq: make solver try hints before stripping away existentialsBrian Campbell
2018-12-23Remove a comment that breaks Isabelle buildThomas Bauereiss
2018-12-22Added RISC-V fence.tsoShaked Flur
2018-12-20RISVC model is now at https://github.com/rems-project/sail-riscv . Remove it ...Robert Norton
2018-12-19Coq: handle pairs of ranges (and other existential types) properlyBrian Campbell
2018-12-19Coq: add zeros library function (used by MIPS)Brian Campbell
2018-12-19Coq: handle existentials in hypotheses during solving, add max_nat, better castsBrian Campbell
2018-12-18Check more carefully for recursive functions when generating LemThomas Bauereiss
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
2018-12-14Add some experimental support for non-lexical flow-typing rulesAlasdair Armstrong
2018-12-14Add a few more tests for JenkinsAlasdair Armstrong
2018-12-14Prepare for new release.Robert Norton
2018-12-14Add truncateLSB builtin useful for implementing Cheri Concentrate. Also add b...Robert Norton
2018-12-14Get real number tests working in OCaml/InterpreterAlasdair
2018-12-14A few additional testsAlasdair
2018-12-13Fix typo in boolean constraint desugaringAlasdair Armstrong
2018-12-13Remove redundant zero extensions more aggressively in mono rewritesThomas Bauereiss
2018-12-13Fix issue with sizeof-rewriting and monomorphisationAlasdair Armstrong
2018-12-13Fixing rationals in Sail interpreter and OCamlAlasdair Armstrong
2018-12-13Add hooks to call cgen stub file for RISC-VAlasdair Armstrong
2018-12-13Add a stub file for future cgen generationsAlasdair Armstrong
2018-12-13Merge remote-tracking branch 'origin/sail2' into asl_flowAlasdair
2018-12-12Fix some small bugsAlasdair
2018-12-12Add parallelism limit to C and builtins testAlasdair Armstrong
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
2018-12-12Add a test for flow typing as found in the ARM 32-bit instructionsAlasdair Armstrong
2018-12-12Add a test case for various simple boolean propertiesAlasdair Armstrong
2018-12-12Get typechecking example with boolean argument flow-typing workingAlasdair
2018-12-12Generalise existentials for non-integer type variablesAlasdair
2018-12-12Remove KOpt_none constructorAlasdair
2018-12-12Fix various boolean type-variable related issuesAlasdair
2018-12-11Fix all tests with type checking changesAlasdair Armstrong
2018-12-11Initial attempt at using termination measures in CoqBrian Campbell
2018-12-11Fix most remaining tests on branchAlasdair
2018-12-10Various changes:Alasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:17:05 +0000