summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2018-09-06Coq: fill in a few more RISC-V axiomsBrian Campbell
2018-09-06Coq: more string handlingBrian Campbell
2018-09-06Coq: fix up some barrier/memory definitions for RISC-VBrian Campbell
2018-09-06RISCV: Get enough of the RISCV platform into C to run some testsAlasdair Armstrong
2018-09-05Coq: fill in trivial ranges in constraint solverBrian Campbell
2018-09-04C: Tweaks to RISC-V to get compiling to CAlasdair Armstrong
2018-09-03Coq: solver should split earlierBrian Campbell
2018-09-03Coq: get top-level value definitions to work nicely againBrian Campbell
2018-09-03Coq: rework generation of dependent pairs so that they are onlyBrian Campbell
2018-08-30Annotate the RISC-V prelude for C builtins.Prashanth Mundkur
2018-08-30C: Fix a bug where function argument type becomes more specific due to flow t...Alasdair Armstrong
2018-08-30Coq: correct endianness reversal bugBrian Campbell
2018-08-29C: Fix some issues with tuples as arguments to polymorphic constructorsAlasdair Armstrong
2018-08-29Updated snapshots for Isabelle 2018Thomas Bauereiss
2018-08-28Coq: make some library definitions computeBrian Campbell
2018-08-28Adapt theory imports for Isabelle 2018Thomas Bauereiss
2018-08-20Add some more test cases for C compilationAlasdair Armstrong
2018-08-15Get RISC-V on Coq into reasonable state to showBrian Campbell
2018-08-14Coq: attempt a quick proof before an indepth oneBrian Campbell
2018-08-14Merge remote-tracking branch 'origin/sail2' into polymorphic_variantsAlasdair Armstrong
2018-08-13Coq: more strings for RISC-VBrian Campbell
2018-08-13Coq: drop irrelevant definitions before constraint solvingBrian Campbell
2018-08-10Coq: add some of string libraryBrian Campbell
2018-08-09Coq: a bit more handling of unknown constraintsBrian Campbell
2018-08-07Improve cast introduction for LemBrian Campbell
2018-08-06Cast each argument to a polymorphic constructor into it's most general typeAlasdair Armstrong
2018-08-03Coq: use a dummy constraint when the real one is unknownBrian Campbell
2018-08-03Coq: generalise dependent pair handling a littleBrian Campbell
2018-08-02Coq: limit eauto to ensure termination in reasonable timeBrian Campbell
2018-08-02Fill in more Coq builtins for aarch64Brian Campbell
2018-08-02Update a few prover gitignoresBrian Campbell
2018-08-01Coq: implicit range conversions for function arguments, debug tracingBrian Campbell
2018-07-23RTS: make g_cycle_count publicAlastair Reid
2018-07-18Coq: constraint solving improvementsBrian Campbell
2018-07-17Coq: integer shiftsBrian Campbell
2018-07-17Coq: add printing stubsBrian Campbell
2018-07-17Coq: handle E_constraint properlyBrian Campbell
2018-07-16Coq: add support for more complex atom typesBrian Campbell
2018-07-13Merge branch 'sail2' of github.com:rems-project/sail into sail2Brian Campbell
2018-07-12Add missing builtins needed for cheri128 C. Still doesn't build possibly due ...Robert Norton
2018-07-12update arm and mips models for new type of write_ram builtin. Also fix c and ...Robert Norton
2018-07-12Coq: handle all bool conjunctions/disjunctionsBrian Campbell
2018-07-12Coq: remove unnecessary constraint on foreach loopsBrian Campbell
2018-07-11Partially revert change to add_vec_int et alThomas Bauereiss
2018-07-11Fix off-by-one bugs in monomorphisation rewrites involving bitvector subrangesThomas Bauereiss
2018-07-11Fix some signedness bugsThomas Bauereiss
2018-07-10Update HOL setupBrian Campbell
2018-07-10Add more Isabelle lemmas to libraryThomas Bauereiss
2018-07-09Changes for anonymisation. Ensure headers are in correct format. Remove some ...Robert Norton
2018-07-09Update gitignoreThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 01:28:50 +0000