summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-07-18Support DMB/DSB domainsShaked Flur
2019-07-16Fix all remaining tests for this branchAlasdair
2019-07-16Get monomorphisation tests working with separate bitvectorsAlasdair Armstrong
2019-07-16Merge remote-tracking branch 'origin/sail2' into separate_bvAlasdair Armstrong
2019-07-11Make sure we do constant-fold primitives howeverAlasdair Armstrong
2019-07-11Make sure constant folding won't fold external definitions that also have sai...Alasdair Armstrong
2019-07-03Consider references in topological sortingThomas Bauereiss
2019-06-30Fix bug with toplevel pattern in RISC-V duopodAlasdair
2019-06-28Monomorphisation: add some alternative names for ones and zero_extend as used...Robert Norton
2019-06-28ToFromInterp backend: always wrap typ arg values in a function, fixes option ...Jon French
2019-06-28Add a warning for potentially unsafe castsAlasdair
2019-06-27SMT: Add a reverse endianness function and fix some bugsAlasdair Armstrong
2019-06-26Fix: Make sure to consider NC_app when checking constraints are identicalAlasdair Armstrong
2019-06-26Make sure we take constraint synonyms into account when checking if types are...Alasdair Armstrong
2019-06-25SMT: Add another case to appendAlasdair Armstrong
2019-06-21Coq: add missing property derivation casts for effectful expressionsBrian Campbell
2019-06-21Coq: be more careful when dealing with wildcard argument patternsBrian Campbell
2019-06-20Coq: avoid more unnecessary uses of pattern bindersBrian Campbell
2019-06-20Coq: handle wildcard binders of bools properlyBrian Campbell
2019-06-20Add additional case to append for Sail -> SMTAlasdair Armstrong
2019-06-20Add more cases to signed for Sail SMTAlasdair Armstrong
2019-06-20Handle more uses of mutable variables during monomorphisation cast insertionBrian Campbell
2019-06-19Make C emulator exit with failure for uncaught exception. Make special case f...Robert Norton
2019-06-19Make default ocaml main exit with non-zero exit code in case of uncaught exce...Robert Norton
2019-06-19Fix buggy ocaml implementation of count_leading_zeros and also make tail recu...Robert Norton
2019-06-19Rewriting improvements for monomorphic aarch64_smallBrian Campbell
2019-06-19Monomorphisation improvements for aarch64_smallBrian Campbell
2019-06-18Fix handling of E_internal_plet in rewriteThomas Bauereiss
2019-06-18Implement count_leading_zeros in LemThomas Bauereiss
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-13Add AST for greater-than and less-than constraintsBrian Campbell
2019-06-12Handle partial matches in guarded pattern rewriteThomas Bauereiss
2019-06-12SMT: Fix missing case for append builtinAlasdair Armstrong
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-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-06Add an option to pre-compile the axiomatic model for SMTAlasdair Armstrong
2019-06-06Update aarch64_small hgen filesAlasdair Armstrong
2019-06-05Add some regression testsAlasdair
2019-06-05Fix: Make sure we check Jib types match for operators before optimizingAlasdair Armstrong
2019-06-05Coq: fix type alias expansion in constraintsBrian Campbell
2019-06-04Make sure aarch64_small can generate Jib for SMTAlasdair Armstrong
2019-06-04Merge branch 'sail2' into separate_bvAlasdair Armstrong
2019-06-04Remove unused AST constructorAlasdair Armstrong