summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
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
2019-11-29Coq: switch to boolean predicates for Sail-type propertiesBrian Campbell
2019-11-21Implement -cycle-limit option for OCaml emulator similar to one for C.Robert Norton
2019-11-20Coq: port a couple of definitions from Isabelle for address translation specBrian Campbell
2019-11-14Update location of sail2_instr_kinds.lemRobert Norton
2019-11-14Perform isabelle check only when heap-img rule is used to avoid calling opam ...Robert Norton
2019-11-13Coq: more proof supportBrian Campbell
2019-11-04Coq: compatiblity with 8.10 as well as 8.9Brian Campbell
2019-10-25Coq: make sure solver can't accidentally use recursive definitionsBrian Campbell
2019-10-24Coq: use `abstract` to separate out proofs from definitionsBrian Campbell
2019-10-18Coq: tweak a state monad lifting rule to improve performanceBrian Campbell
2019-10-17Allow generating C that doesn't hard code any librariesAlasdair Armstrong
2019-10-16Now builds arm address translation with clang -target aarch64-none-eabiAlasdair Armstrong
2019-10-16Make nostd Sail arena allocator thread safe (maybe)Alasdair
2019-10-15More work on bare-metal SailAlasdair Armstrong
2019-10-14Add -Ofixed_int and -Ofixed_bits to assume fixed-precision ints and bitvector...Alasdair Armstrong
2019-10-02Coq: generate decidable equality instances for variant typesBrian Campbell
2019-10-02Coq: limited support for existentially-typed tuplesBrian Campbell
2019-09-19Change Coq Hoare logic rules to produce nicer preconditionsBrian Campbell
2019-09-19Expand Coq Hoare logic and congruence rules to more operatorsBrian Campbell
2019-09-02Coq: add properly checked subrange update, reduce importsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:02:42 +0000