summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-01-31Drop type annotations in top-level nexp rewriting in favour of valspecsBrian Campbell
2019-01-31Make cast insertion handle more complex nexps and pushing casts into blocksBrian Campbell
2019-01-31Monomorphisation: improve cast insertion and nexp rewriting on variantsBrian Campbell
2019-01-31Add missing cases to constraint comparisonBrian Campbell
2019-01-31Support case splitting on variables as well as sizeof in cast introductionBrian Campbell
2019-01-29Improve generation of initial register stateThomas Bauereiss
2019-01-28Lem: Be more careful about nexps occurring in the function signatureThomas Bauereiss
2019-01-25Monomorphisation: update a built-in nameBrian Campbell
2019-01-25Fix solution finding using SMT by looking for the right variableBrian Campbell
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-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-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add parens around negative integer literalsBrian Campbell
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-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-23Remove a comment that breaks Isabelle buildThomas Bauereiss
2018-12-22Added RISC-V fence.tsoShaked Flur
2018-12-19Coq: handle pairs of ranges (and other existential types) properlyBrian 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:09:10 +0000