summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-04-17Remove obsolete generated files from .gitignore directory so they will show u...Robert Norton
2019-04-17Allow libsail to be installed without the other things (for rmem)Shaked Flur
2019-04-17Build libsail again (removed Bytcode and Share_directory)Shaked Flur
2019-04-16Temporarily remove Makefile part that is making Jenkins failAlasdair Armstrong
2019-04-16Fix: Don't repeat ctyp_of_typ callAlasdair Armstrong
2019-04-16Remove unnecessary assertThomas Bauereiss
2019-04-16SMT: Support toplevel letbindingsAlasdair Armstrong
2019-04-16SMT: Fix inlining issuesAlasdair Armstrong
2019-04-16Code for testing builtins with CoqBrian Campbell
2019-04-16Coq: make bools_of_int (and hence get_slice_int) compute wellBrian Campbell
2019-04-16Coq: set_slice typoBrian Campbell
2019-04-16Coq: tdiv builtinsBrian Campbell
2019-04-16Coq: add specialised shiftsBrian Campbell
2019-04-16Coq: don't record assertions in the context if Sail doesn'tBrian Campbell
2019-04-16Also allow "repeat" in loop termination measure syntaxBrian Campbell
2019-04-16BugfixingThomas Bauereiss
2019-04-16SMT: Take care to not generate duplicate labelsThomas Bauereiss
2019-04-16SMT: Add struct value literalsAlasdair
2019-04-15Add more SMT builtinsThomas Bauereiss
2019-04-15SMT: Allow partial specializationsAlasdair Armstrong
2019-04-15Merge branch 'sail2' of github.com:rems-project/sail into sail2Jon French
2019-04-15Merge branch 'sail2' into rmem_interpreterJon French
2019-04-15Fix: Allow zero-length vector literalsAlasdair Armstrong
2019-04-15Basic loop termination measures for CoqBrian Campbell
2019-04-13SMT: Add count_leading_zeros and more builtinsAlasdair
2019-04-13SMT: More builtinsAlasdair
2019-04-12ToFromInterp_backend: print type annotations for abbrevs of unquantified type...Jon French
2019-04-12ToFromInterp_backend: don't generate converters for cache_op_kindJon French
2019-04-12ToFromInterp_backend: better handling of nexpsJon French
2019-04-12lib/regfp.sail: add explicit C binding for memory access functionsJon French
2019-04-12Interpreter: remove debug printing (oops)Jon French
2019-04-12update libsail.mllib with more jib modulesJon French
2019-04-11SMT: Add property and counterexample directiveAlasdair Armstrong
2019-04-11SMT: Fixes for more cheri compressed cap propertiesAlasdair
2019-04-10SMT: More builtins and testsAlasdair Armstrong
2019-04-10Coq: update prompt monad to match the Lem, and port the state monad/liftingBrian Campbell
2019-04-10Coq: tweak measure rewrites slightlyBrian Campbell
2019-04-10SMT: Add some simple constant folding for generated SMTAlasdair
2019-04-09SMT: Refactor Jib values to make inlining workAlasdair Armstrong
2019-04-09SMT: Experimental Jib->SMT translationAlasdair Armstrong
2019-04-06Various bugfixes and improvementsAlasdair
2019-04-05Coq: termination measures for mutually recursive functionsBrian Campbell
2019-04-05Fix: Don't remove uncalled polymorphic constructors if they are matched uponAlasdair Armstrong
2019-04-05Fix: Add test case for commit 689eaeAlasdair Armstrong
2019-04-05Coq: add missing effectful existential unpacking caseBrian Campbell
2019-04-05Lem: Make generated assertion messages look nicer in prover outputAlasdair
2019-04-04AArch64: Update write_mem_val to write_memAlasdair
2019-04-04Coq: improve solver on conjunctions, Euclidean division/moduloBrian Campbell
2019-04-04Coq: correct projection in plain monadic and/orBrian Campbell
2019-04-04Typecheck: Improve typechecking for constructors with tuple typesAlasdair
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 05:22:38 +0000