summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
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-09Coq: the division used in smt.sail should be EuclideanBrian Campbell
2019-01-09Coq: add truncateLSB and import Zeuclid by defaultBrian Campbell
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-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-11-30Parser tweaks and fixesAlasdair Armstrong
2018-11-30Improvements for ASL parserAlasdair Armstrong
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:00:58 +0000