summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-05-06Cope with irrelevant existentials when monomorphising constructorsBrian Campbell
2019-05-06Don't initialise registers in interpreter when register accesses not allowedBrian Campbell
2019-05-06Expand constraints while looking for sets during monomorphisationBrian Campbell
2019-04-26Fix some broken interpreter testsAlasdair Armstrong
2019-04-26More constructor monomorphisation supportBrian Campbell
2019-04-25Fill in missing map_..._annot caseBrian Campbell
2019-04-25More read/write function updatesBrian Campbell
2019-04-25Get basic constructor monomorphisation working againBrian Campbell
2019-04-25Make constructor splitting in monomorphisation obey -dall_split_errorsBrian Campbell
2019-04-25Don't try to insert monomorphisation casts when the types are the sameBrian Campbell
2019-04-25lem gen_lib: update read/write functions to take (dummy) addrsize argument as...Jon French
2019-04-20Fix: Reduce constant-fold time for ARM from 20min+ to 10sAlasdair Armstrong
2019-04-19Coq: when replacing n_constraints in types allow for some rearrangementBrian Campbell
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
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-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-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-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-12Interpreter: remove debug printing (oops)Jon French
2019-04-12update libsail.mllib with more jib modulesJon French
2019-04-10Coq: tweak measure rewrites slightlyBrian Campbell
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-05Coq: add missing effectful existential unpacking caseBrian Campbell
2019-04-05Lem: Make generated assertion messages look nicer in prover outputAlasdair
2019-04-04Coq: correct projection in plain monadic and/orBrian Campbell
2019-04-04Typecheck: Improve typechecking for constructors with tuple typesAlasdair
2019-04-02Coq: replace n_constraints with equivalent bool variablesBrian Campbell
2019-04-01C: Fix end instr usage in jib_optimizeAlasdair Armstrong
2019-04-01C: Add identifier to end instructionAlasdair
2019-03-27C: Generate C from sliced specificationsAlasdair Armstrong
2019-03-27Interactive: Refactor sail.ml some moreAlasdair Armstrong
2019-03-27Interactive: Refactor sail.mlAlasdair Armstrong
2019-03-27Rewriter: Finish refactoring rewrite sequencesAlasdair Armstrong
2019-03-26Rewriter: Expose rewrite passes to interactive modeAlasdair Armstrong
2019-03-26Constant-fold __size calls if possibleThomas Bauereiss
2019-03-26Lem: Work around if-cascade indentation problemThomas Bauereiss
2019-03-25Typecheck: Use emod_int/ediv_int in sizeof rewritingAlasdair Armstrong
2019-03-22Tidy up of div and mod operators (C implementation was previously inconsisten...Robert Norton
2019-03-22C: Fix as-patterns in C outputAlasdair Armstrong
2019-03-21Fix: Use doc_binding for printing scattered mapping typesAlasdair Armstrong
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 11:21:10 +0000