summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2019-07-18Update aarch64_small to build with new barriersAlasdair Armstrong
2019-07-18Support DMB/DSB domainsShaked Flur
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
2019-06-27Coq: less constrained version of slice for ARM modelBrian Campbell
2019-06-21Coq: even more robust handling of unknown goalsBrian Campbell
2019-06-21Coq: better handling of unknown constraintsBrian Campbell
2019-06-20Coq: avoid some unnecessary reduction in the constraint solverBrian Campbell
2019-06-19Monomorphisation improvements for aarch64_smallBrian Campbell
2019-06-17Add sail implementation of count_leading_zeros. We could use this for backend...Robert Norton
2019-06-17Implement a count_leading_zeros builtin for ocaml and c. This may be a slight...Robert Norton
2019-06-13Coq: add eq_bit built-inBrian Campbell
2019-06-12Fix Lem binding for abs_intThomas Bauereiss
2019-06-11Coq: add concatenation operator for polymorphic vectorsBrian Campbell
2019-06-06Coq: more aggressive rewriting before solvingBrian Campbell
2019-06-06Coq: tweak bool to Z to use less memoryBrian Campbell
2019-06-06Fix tdiv_int and tmod_int bindings for LemThomas Bauereiss
2019-06-06Add arith_shiftr to C and OCaml librariesThomas Bauereiss
2019-06-05Coq: exploit arithmetic solver for some mixed integer/bool problems.Brian Campbell
2019-06-05Coq: generalize proof terms before main solverBrian Campbell
2019-06-04Coq: more constraint solvingBrian Campbell
2019-06-03Coq: experiment with another boolean iff solving methodBrian Campbell
2019-05-30Set interpreter builtin for truncateLSB.Robert Norton
2019-05-29Coq: more solver improvementsBrian Campbell
2019-05-29Coq: need a proof for _shr32Brian Campbell
2019-05-28Coq: more constraint solvingBrian Campbell
2019-05-24Coq: switch to computable versions of BBV shiftsBrian Campbell
2019-05-23Coq: solve some division constraintsBrian Campbell
2019-05-23Coq: define the names from the Sail real libraryBrian Campbell
2019-05-23Fix bug in slice_maskThomas Bauereiss
2019-05-22Coq: tweak disjunctions tactic with subst to support more constraintsBrian Campbell
2019-05-21Coq: remove premature unfolding of local definitionsBrian Campbell
2019-05-20Coq: fix property extraction bug, solve some constraints involving setsBrian Campbell
2019-05-19Coq: add signed bitvector to integer function that doesn't need >0 constraintBrian Campbell
2019-05-19Coq: proper definitions for some undefined value functionsBrian Campbell
2019-05-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
2019-05-15Coq: constraint solving for aarch64Brian Campbell
2019-05-14Various bugfixesAlasdair Armstrong
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14Add feature that allows functions to require type variables are constantAlasdair Armstrong
2019-05-13Merge branch 'sail2' into smt_experimentsAlasdair
2019-05-13Parse dereferences in orderinary expressionsAlasdair
2019-05-13fix typo in excl_res externJon French
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 08:54:17 +0000