summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-10SMT: Experiment with symbolic memory reads and writesAlasdair Armstrong
2019-05-09SMT: Make path conditionals more preciseAlasdair Armstrong
2019-05-08Remove generated TeX fileThomas Bauereiss
2019-05-07Merge branch 'sail2' into smt_experimentsAlasdair Armstrong
2019-05-07Patch up a couple of Isabelle proofs due to memory interface changesBrian Campbell
2019-05-05C: Add option to compile using __int128 rather than GMPAlasdair
2019-05-03Jib: Optimize set_slice for ARM v8.5Alasdair Armstrong
2019-05-03Jib: Fix optimizations for SMT IR changesAlasdair Armstrong
2019-04-27Merge branch 'sail2' into smt_experimentsAlasdair
2019-04-26Fix some broken interpreter testsAlasdair Armstrong
2019-04-25Update coq read_mem/write_mem.Prashanth Mundkur
2019-04-25More read/write function updatesBrian Campbell
2019-04-24SMT: Make sure we clear overflow checks between generating propertiesAlasdair Armstrong
2019-04-19Coq: more robust handling of unknown constraintsBrian Campbell
2019-04-18Parameterise memory read/write primitives by address lengthJon French
2019-04-17Add interpreter annots to vector_dec.Prashanth Mundkur
2019-04-17now without memory leaksJon French
2019-04-17add unimplemented C platform definitions for platform_read_mem etcJon French
2019-04-17SMT: Unroll simple foreach loopsAlasdair Armstrong
2019-04-16Coq: make bools_of_int (and hence get_slice_int) compute wellBrian Campbell
2019-04-16Coq: set_slice typoBrian Campbell
2019-04-16Coq: tdiv builtinsBrian Campbell
2019-04-16Coq: add specialised shiftsBrian Campbell
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-12lib/regfp.sail: add explicit C binding for memory access functionsJon French
2019-04-10Coq: update prompt monad to match the Lem, and port the state monad/liftingBrian Campbell
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-04-04Coq: improve solver on conjunctions, Euclidean division/moduloBrian Campbell
2019-03-27Coq: add a little knowledge about ZEuclid.divBrian Campbell
2019-03-27Coq: replace firstorder with less expensive tacticsBrian Campbell
2019-03-22Tidy up of div and mod operators (C implementation was previously inconsisten...Robert Norton
2019-03-19Coq: more test workBrian Campbell
2019-03-19Coq: more work on testsBrian Campbell
2019-03-18Add non-negative constraints for zeros/onesBrian Campbell
2019-03-15Various monomorphisation tweaks and fixesThomas Bauereiss
2019-03-15Make mono_rewrites less dependant on ASL preludeThomas Bauereiss
2019-03-15Coq: some progress on the test suiteBrian Campbell
2019-03-15Coq: better loop handling, discharge some related proof obligationsBrian Campbell
2019-03-14Merge branch 'sail2' into rmem_interpreterJon French
2019-03-13lib/regfp.sail: new standard intrinsics for triggering memory effectsJon French
2019-03-13C: Add missing update_lbits builtinAlasdair Armstrong
2019-03-12Coq: try non-linear nia solver tooBrian Campbell
2019-03-12Coq: fix some boolean issues seen in armBrian Campbell
2019-03-08Fix the Coq mapping for eq_string in Sail lib.Prashanth Mundkur
2019-03-08Adds the DC and IC instructions to AArch64_small;Shaked Flur
2019-03-07Fix bug in a mono rewrite helper functionThomas Bauereiss
2019-03-07Coq: apply a little brute force in some boolean goalsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:31:23 +0000