summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
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
2019-08-29Turn the two abs_int declarations into overloadsBrian Campbell
2019-08-22Coq: tactics to do rewrites under state monad, simple wp computationBrian Campbell
2019-08-19Coq: add bools_of_bits_nondet and friends to libraryBrian Campbell
2019-08-14Use bitvector type in mono rewritesThomas Bauereiss
2019-08-14Fix bug in mono rewritesThomas Bauereiss
2019-08-14Coq library work for proofs:Brian Campbell
2019-08-13Coq: definitions for cheri128 modelBrian Campbell
2019-08-02Fix up some edge cases with the bitvector/polyvector splitBrian Campbell
2019-08-01Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-07-31Coq: Update barrier definitionsBrian Campbell
2019-07-31Coq: tweak Hoare proofs a littleBrian Campbell
2019-07-31Coq: reasoning for until loopsBrian Campbell
2019-07-31Merge branch 'sail2' into union_barrierAlasdair Armstrong
2019-07-31Remove redundant ifdef and run SMT tests by defaultAlasdair Armstrong
2019-07-31Change platform_barrier so it doesn't care about it's argument typeAlasdair Armstrong
2019-07-29Coq: add state monad version of while/until loops and lifting resultsBrian Campbell
2019-07-25Update Coq barrier definitionBrian Campbell
2019-07-25Basic port of proof machinery to CoqBrian Campbell
2019-07-18Need to separate out the 0.10 lem library from upcoming 0.11Alasdair Armstrong
2019-07-18Add a feature flag for barrier type changeAlasdair Armstrong
2019-07-18Update aarch64_small to build with new barriersAlasdair Armstrong
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-16Fix all remaining tests for this branchAlasdair
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-07-15Add a fast path to speed up platform_read_ram: use fast_read_ram if read is 8...Robert Norton
2019-07-04Add coq builtin for concat_str (copied from mips prelude).Robert Norton
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:02:50 +0000