summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-05-21Fix: undefined_nat test for interpreterAlasdair Armstrong
2019-05-21SMT: Add control flow node numbers to memory events to track program orderAlasdair Armstrong
2019-05-21Lem: Fix bug in generation of val-specsThomas Bauereiss
2019-05-21Coq: remove premature unfolding of local definitionsBrian Campbell
2019-05-21Coq: introduce autocasts at variablesBrian Campbell
2019-05-20Coq: fix property extraction bug, solve some constraints involving setsBrian Campbell
2019-05-20Revert "Add constraints to undefined vector functions to ensure that lengths ...Brian Campbell
2019-05-20Filter termination measures during slicingBrian Campbell
2019-05-20Speed up graph construction by always keeping graph in normalized formBrian Campbell
2019-05-20Coq: add some missing autocasts, avoid unnecessary patterns in letsBrian Campbell
2019-05-19Coq: add signed bitvector to integer function that doesn't need >0 constraintBrian Campbell
2019-05-19Coq: remove unhelpful type printing restriction on early returnsBrian Campbell
2019-05-19Coq: proper definitions for some undefined value functionsBrian Campbell
2019-05-19Add constraints to undefined vector functions to ensure that lengths areBrian Campbell
2019-05-17Get all Lem tests working with separate bitvector typeAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 10:43:33 +0000