summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2019-03-15Coq: some progress on the test suiteBrian Campbell
2019-03-15Coq: better loop handling, discharge some related proof obligationsBrian Campbell
2019-03-13C: Add missing update_lbits builtinAlasdair Armstrong
2019-03-12Coq: try non-linear nia solver tooBrian Campbell
2019-03-12Coq: fix some boolean issues seen in armBrian Campbell
2019-03-08Fix the Coq mapping for eq_string in Sail lib.Prashanth Mundkur
2019-03-08Adds the DC and IC instructions to AArch64_small;Shaked Flur
2019-03-07Fix bug in a mono rewrite helper functionThomas Bauereiss
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
2019-03-05Coq: firstorder is better at the boolean goalsBrian Campbell
2019-03-05Coq: use setoid rewriting to apply under an existential binderBrian Campbell
2019-03-05Coq 8.9 compatibility fixBrian Campbell
2019-03-05Additional optimizations for C compilationAlasdair
2019-03-01Coq: some library compatibility changesBrian Campbell
2019-03-01Coq: add a little bit of boolean solvingBrian Campbell
2019-02-28Coq: remove unused library definitionsBrian Campbell
2019-02-28Coq: Clean up rich boolean handling in backendBrian Campbell
2019-02-28Coq: more for informative booleansBrian Campbell
2019-02-28Coq: some work on bool simplificationBrian Campbell
2019-02-25Fix some builtins, and make mod_int return naturalAlasdair Armstrong
2019-02-21Allow monomorphisation with C generationAlasdair
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:25:10 +0000