summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-05-28Coq: more constraint solvingBrian Campbell
2019-05-28Coq: don't output complex bool types at let expressionsBrian Campbell
2019-05-28Just build lem in aarch64_small testAlasdair Armstrong
2019-05-28SMT: Add min and max functionsAlasdair Armstrong
2019-05-28Make sure single clause functions with top-level guards work correctlyAlasdair Armstrong
2019-05-24Add a :thin_slice command to isail to isolate a given set of functionsBrian Campbell
2019-05-24Coq: support if-then-throw typechecking special caseBrian Campbell
2019-05-24Coq: switch to computable versions of BBV shiftsBrian Campbell
2019-05-23Coq: support loops which update richly typed variablesBrian 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-22Coq: replace inferrable integer arguments with _ at more typesBrian Campbell
2019-05-22Use opam instructions in INSTALL.mdAlasdair Armstrong
2019-05-22Fix: Update INSTALL.md with opam switch instructionsAlasdair Armstrong
2019-05-22Move Util.warn to Reporting, and make it take the location as a parameterAlasdair Armstrong
2019-05-21SMT: Use a separate constructor for memory read variablesAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:44:43 +0000