summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-17Implement a count_leading_zeros builtin for ocaml and c. This may be a slight...Robert Norton
2019-06-13Fix some bugs in Lem rewriterThomas Bauereiss
2019-06-13Add new option to splice in alternative function definitionsBrian Campbell
2019-06-13Coq: add eq_bit built-inBrian Campbell
2019-06-13Add AST for greater-than and less-than constraintsBrian Campbell
2019-06-12Fix Lem binding for abs_intThomas Bauereiss
2019-06-12Handle partial matches in guarded pattern rewriteThomas Bauereiss
2019-06-12SMT: Fix missing case for append builtinAlasdair Armstrong
2019-06-11Coq: add concatenation operator for polymorphic vectorsBrian Campbell
2019-06-11Coq: improve readability of types filesBrian Campbell
2019-06-10Add well-formedness check for type schemes in valspecs.Brian Campbell
2019-06-08Workaround for OCaml bytecode memory bugBrian Campbell
2019-06-06Fix aarch64_small testAlasdair Armstrong
2019-06-06Coq: more aggressive rewriting before solvingBrian Campbell
2019-06-06Coq: tweak bool to Z to use less memoryBrian Campbell
2019-06-06SMT: Rename some functions to make usage clearerAlasdair Armstrong
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-06SMT: Add function to de-serialise serialised modelAlasdair Armstrong
2019-06-06Fix aarch64_small makefileAlasdair Armstrong
2019-06-06Add an option to pre-compile the axiomatic model for SMTAlasdair Armstrong
2019-06-06Update aarch64_small hgen filesAlasdair Armstrong
2019-06-06update funding acksPeter Sewell
2019-06-05Add some regression testsAlasdair
2019-06-05Coq: exploit arithmetic solver for some mixed integer/bool problems.Brian Campbell
2019-06-05Fix: Make sure we check Jib types match for operators before optimizingAlasdair Armstrong
2019-06-05Coq: generalize proof terms before main solverBrian Campbell
2019-06-05Coq: fix type alias expansion in constraintsBrian Campbell
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong
2019-06-04Coq: more constraint solvingBrian Campbell
2019-06-04Merge pull request #52 from scottj97/update-gitignoreAlasdair Armstrong
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-06-03Add new files to .gitignoreScott Johnson
2019-06-03Test case for previous commitBrian Campbell
2019-06-03Coq: support non-exhaustive pattern rewrite for exception handlingBrian Campbell
2019-06-03Coq: experiment with another boolean iff solving methodBrian Campbell
2019-05-31Add SMT related things to libsail fileAlasdair Armstrong
2019-05-31Change specialization interface slightlyAlasdair Armstrong
2019-05-30Implement ones builtin in sail_lib and add to interpreter. However currently ...Robert Norton
2019-05-30Set interpreter builtin for truncateLSB.Robert Norton
2019-05-29Some minor grammar fixes in internals.mdAlasdair Armstrong
2019-05-29Fix some typosAlasdair Armstrong
2019-05-29Add some Sail internals documentationAlasdair Armstrong
2019-05-29Coq: more solver improvementsBrian Campbell
2019-05-29Coq: need a proof for _shr32Brian Campbell
2019-05-29SMT: Make bitvector equality work between vectors of different lengthsAlasdair Armstrong
2019-05-29SMT: Fix sail_truncate and sail_mask for unusual argument typesAlasdair Armstrong
2019-05-29Fix sail_truncate error message in SMTAlasdair Armstrong
2019-05-28Fix typechecking test expected errorAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:33:20 +0000