summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-17SMT: Finish adding all memory builtins from lib/regfp.sailAlasdair Armstrong
2019-05-16Fix: Add a feature symbol for new constant type variable syntaxAlasdair Armstrong
2019-05-16SMT: Tweak SMT generation interfaceAlasdair Armstrong
2019-05-16SMT: Improve simplification for generated SMTAlasdair Armstrong
2019-05-1594f445 introduced a new name for _ref_deref, add it to the effect rewritingBrian Campbell
2019-05-15Coq: constraint solving for aarch64Brian Campbell
2019-05-14SMT: Allow printing SMT with an optional variable prefixAlasdair Armstrong
2019-05-14Fix test case for previous commitAlasdair Armstrong
2019-05-14Various bugfixesAlasdair Armstrong
2019-05-14Merge branch 'smt_experiments' into sail2Alasdair Armstrong
2019-05-14SMT: Add comment explaining path conditionalsAlasdair Armstrong
2019-05-14Fix: Issue a warning for any unrecognised directiveAlasdair 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-13aarch64_small: correct cast_bool_bit/cast_bit_bool functionsJon French
2019-05-13aarch64_small: convert memory access functions to use sail2 primitivesJon French
2019-05-13aarch64_small: remove spurious extra declaration of _rPCJon French
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:38:32 +0000