summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2020-11-19Add write tag primitiveBrian Campbell
2020-10-14Support C coverage when sail_exit is usedBrian Campbell
2020-10-01pass pointer to g_elf_entry to get the ELF entrySander Huyghebaert
2020-09-30Tweak Coq proof to avoid incompatibility with IrisBrian Campbell
2020-09-12Merge some of the gitignore filesColumbus240
2020-09-07Fix typo a mono_rewrites definitionBrian Campbell
2020-09-07Correct external declaration in mono_rewritesBrian Campbell
2020-08-26Coq: replace other uses of omega with liaBrian Campbell
2020-08-26Coq: replace a lot of omega with liaBrian Campbell
2020-08-26Coq: Use proof mode for a couple of Fixpoints to avoid Coq 8.12 issueBrian Campbell
2020-08-26Coq: make some uses of auto in the library more robustBrian Campbell
2020-08-25Add function sail_set_coverage_file to sail_coverage headerAlasdair
2020-08-18Move sail_state declaration into it's own fileAlasdair
2020-08-07Merge branch 'monads' into sail2Brian Campbell
2020-07-02Define extz/s_vec in Sail for non-prover backendsBrian Campbell
2020-06-24Add tagged memory builtins to regfp.sailThomas Bauereiss
2020-06-17Coq: implement shl_int_1Brian Campbell
2020-06-14Coq: tidy up scope in libraryBrian Campbell
2020-06-12Coq: fix matching bug in solverBrian Campbell
2020-06-11Coq: specialise the andor solvers to avoid excessive search and solve more goalsBrian Campbell
2020-06-10Prepare Coq library for packagingBrian Campbell
2020-05-21Merge branch 'mono-tweaks' of github.com:rems-project/sail into mono-tweaksAlasdair
2020-05-21Merge branch 'sail2' into mono-tweaksAlasdair
2020-05-15Add coverage headerAlasdair
2020-05-15Add coverage tracking toolAlasdair
2020-05-14Merge remote-tracking branch 'origin' into codegenAlasdair
2020-05-14Various bugfixes and improvements for updated codegenAlasdair
2020-05-13Make Isabelle lemma generation work with grouped regstateThomas Bauereiss
2020-05-11Functorise and refactor C code generatorAlasdair
2020-04-28Add flooring division in preludeAlasdair
2020-04-21Fix sub_bits interpreter bindingThomas Bauereiss
2020-04-21Add more monomorphisation rewritesThomas Bauereiss
2020-04-21Add support for some ASL idioms in mono rewritesThomas Bauereiss
2020-04-21Add more mono rewrites for bitvector subrangesThomas Bauereiss
2020-04-10Add Lem builtins for operations on realsThomas Bauereiss
2020-04-10Update path for newer versions of BBV Coq libraryThomas Bauereiss
2020-02-24Allow overloading of subrange builtins for non-bitvectorsThomas Bauereiss
2020-02-21Add barriers to regfp.sail for full ARMv8Alasdair Armstrong
2020-02-05Tweak Coq scopes for 8.11Brian Campbell
2020-02-03Add an __instr_announce builtin in regfp.sailAlasdair Armstrong
2020-02-03Update regfp.sail with ifetch changes from poly_mapping branchAlasdair Armstrong
2020-01-21Use hex/bin literals in Coq backendBrian Campbell
2020-01-17Merge branch 'coq-bool-props' into sail2Brian Campbell
2020-01-17Coq: add hex_strBrian Campbell
2020-01-07Coq: accelerate wp steps by improving application of existing specsBrian Campbell
2019-12-19Coq library improvementsBrian Campbell
2019-12-09Coq: improve solver enough to handle arm specBrian Campbell
2019-12-06Don't introduce uneccesary control flow when compilingAlasdair Armstrong
2019-12-06Coq: use proof irrelevance for a few propertiesBrian Campbell
2019-12-05Coq: more solving support for boolean predicatesBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:52:38 +0000