summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-04Remove unused AST constructorAlasdair Armstrong
2019-06-04SMT: Add a fuzzing tool for the SMT builtinsAlasdair Armstrong
2019-06-03Coq: support non-exhaustive pattern rewrite for exception handlingBrian 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-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-28Coq: don't output complex bool types at let expressionsBrian Campbell
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-23Coq: support loops which update richly typed variablesBrian Campbell
2019-05-22Coq: replace inferrable integer arguments with _ at more typesBrian Campbell
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-13 14:58:50 +0000