summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2019-02-08Add missing functions to HOL monad wrapperThomas Bauereiss
2019-02-07Monomorphisation tweaks for v8.5Thomas Bauereiss
2019-02-06Fix some testsAlasdair Armstrong
2019-02-06Remove all sizeof rewriting from C compilationAlasdair
2019-02-04Fix some warningsAlasdair Armstrong
2019-02-02Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
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-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-29Fixes for full v8.5Alasdair Armstrong
2019-01-29Add a few more type annotations after mono rewritesThomas Bauereiss
2019-01-29Merge branch 'sail2' into asl_flow2Thomas Bauereiss
2019-01-24Start supporting informative bool types in Coq backendBrian Campbell
2019-01-23Don't let "make" fail unnecessarily in lib/isabelleThomas Bauereiss
2019-01-22Don't hardcode location of BBV libraryThomas Bauereiss
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 build of Isabelle documentationThomas Bauereiss
2019-01-14Merge remote-tracking branch 'origin/sail2' into asl_flow2Alasdair
2019-01-10Fixes so 8.5 with vector instructions compiles to CAlasdair Armstrong
2019-01-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Merge sail2 into monadsThomas Bauereiss
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
2019-01-04Add a few helper lemmasThomas Bauereiss
2019-01-04C library: fix fprintf warnings in lib/elf.cAlastair Reid
2019-01-01Coq: update instr_kinds from LemBrian Campbell
2018-12-29Coq: ensure that recursive functions computeBrian Campbell
2018-12-27Coq: make solver try hints before stripping away existentialsBrian Campbell
2018-12-22Added RISC-V fence.tsoShaked Flur
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-18Fix rewriter issuesAlasdair Armstrong
2018-12-18Merge branch 'sail2' into monadsThomas Bauereiss
2018-12-17Changes for ASL parserAlasdair Armstrong
2018-12-17Adapt Coq and termination measure support to typechecker changesBrian Campbell
2018-12-14Add truncateLSB builtin useful for implementing Cheri Concentrate. Also add b...Robert Norton
2018-12-13Remove redundant zero extensions more aggressively in mono rewritesThomas Bauereiss
2018-12-13Fix issue with sizeof-rewriting and monomorphisationAlasdair Armstrong
2018-12-13Merge remote-tracking branch 'origin/sail2' into asl_flowAlasdair
2018-12-12Move much of recursive function termination to a rewriteBrian Campbell
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
2018-12-03Add Write_mem event/outcome without tagThomas Bauereiss
2018-12-03Make names of memory r/w events more consistentThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:42:02 +0000