summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2018-11-30Parser tweaks and fixesAlasdair Armstrong
2018-11-30Rename Undefined outcome to ChooseThomas Bauereiss
2018-11-30Improvements for ASL parserAlasdair Armstrong
2018-11-29Add separate outcome/event for tagged memory loadsThomas Bauereiss
2018-11-29Add some helper lemmas to Isabelle libThomas Bauereiss
2018-11-27Fix memory leak in string_of_bitsAlasdair Armstrong
2018-11-23Introduce intermediate bitvector representation in CAlasdair Armstrong
2018-11-23C backend improvementsAlasdair Armstrong
2018-11-21Coq: min_natBrian Campbell
2018-11-21Coq: add equality for records and polymorphic vectorsBrian Campbell
2018-11-20Use nat instead of (list bitU) for addresses in monad outcomesThomas Bauereiss
2018-11-20Minor coq updatesBrian Campbell
2018-11-20Add full constraints for vector updatesBrian Campbell
2018-11-19Merge branch 'latex' into sail2Robert Norton
2018-11-19Add missing constraints on bitvector_access, with regression test.Fixes #24.Robert Norton
2018-11-16Various bugfixes and a simple profiling feature for rewritesAlasdair Armstrong
2018-11-15document signed and unsignedRobert Norton
2018-11-13Make pretty printer stricter with brace placementAlasdair Armstrong
2018-11-09Improvements to latex generationAlasdair Armstrong
2018-11-07Move inline forall in function definitionsAlasdair Armstrong
2018-11-07Move inline forall in function definitionsAlasdair Armstrong
2018-10-31Fix Isabelle libraryThomas Bauereiss
2018-10-23RTS: Add elf symbol lookup support.Prashanth Mundkur
2018-10-23RTS: allow elf-loader to provide entry info.Prashanth Mundkur
2018-10-22Update Coq patch for RISC-V, add string_take to Coq libraryBrian Campbell
2018-10-16Re-implement space-related mapping functions in Sail rather than backendsJon French
2018-09-28Fix optimisation bug for certain if statementsAlasdair Armstrong
2018-09-19Coq: track changes elsewhereBrian Campbell
2018-09-19Coq: more fixes for AArch64Brian Campbell
2018-09-17Coq: solve some constraint/type errors with AArch64Brian Campbell
2018-09-17Coq: make generic_neq work on realBrian Campbell
2018-09-13Coq: real built-ins for AArch64Brian Campbell
2018-09-12Coq: make generic_eq work on more typesBrian Campbell
2018-09-12Coq: remove extra "True"s from constraintsBrian Campbell
2018-09-11Coq: some basic handling for more existentialsBrian Campbell
2018-09-10Various fixesAlasdair Armstrong
2018-09-07C: Support RISC-V in elf loader.Prashanth Mundkur
2018-09-07C: add a usage message to the rts.Prashanth Mundkur
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:46:39 +0000