summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-02-01Fix missing typedef cases in OCaml outputAlasdair
2019-02-01Add test cases for integer synonymsAlasdair
2019-02-01Expand integer synonymsAlasdair Armstrong
2019-02-01Add tracing instrumention for SMTAlasdair Armstrong
2019-02-01Use same license as Sail for emacs modeAlasdair Armstrong
2019-02-01Merge pull request #29 from thoughtpolice/patch-1Alasdair Armstrong
2019-02-01Tweak HOL LEM_DIR to match riscv makefileBrian Campbell
2019-02-01Make hol libraries use opam Lem library by defaultBrian Campbell
2019-01-31sail-mode: add ELPA metadataAustin Seipp
2019-01-31Fix an unnecessary cast insertion on assignmentsBrian Campbell
2019-01-31Turn on cast insertion for -lem_mwords and revert b826df25Brian Campbell
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-31Build Isabelle heap image instead of just running sessionThomas Bauereiss
2019-01-31Adapt HOL library to monad changesThomas Bauereiss
2019-01-31Merge branch 'monads' into asl_flow2Thomas Bauereiss
2019-01-31Further restrict attention to Int kidsThomas Bauereiss
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-30Cache compilation results to improve build times for repeated buildsAlasdair
2019-01-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add an option to crudely slice a function out of a Sail modelBrian Campbell
2019-01-29Monomorphisation: add missing tyvar substitution during constrant propagationBrian Campbell
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-29Improve generation of initial register stateThomas Bauereiss
2019-01-29Monomorphisation: restrict our attention to Int kidsBrian Campbell
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-25Coq: add enough to generate some output for arm-v8.5-aBrian Campbell
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-24Make recheck_defs_without_effects restore old flag properlyBrian Campbell
2019-01-23Minor opam release to fix #26. Also includes new unrolling pragma.Robert Norton
2019-01-23Don't let "make" fail unnecessarily in lib/isabelleThomas Bauereiss
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 12:28:11 +0000