summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-07Preserve more pattern locations during type checkingBrian Campbell
2019-05-07Patch up a couple of Isabelle proofs due to memory interface changesBrian Campbell
2019-05-06Handle type variables generated while inferring applications in monomorphisationBrian Campbell
2019-05-06Avoid degenerate construction monomorphisation, use # in generated namesBrian Campbell
2019-05-06Apply constructor monomorphisation in preference to variable splitsBrian Campbell
2019-05-06Calculate some type variable substitutions during constant propagationBrian Campbell
2019-05-06Handle global constants in monomorphisationBrian Campbell
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-05-03Tidy of Sail Ott definition to allow valid Isabelle datatypes to be generated...Mark Wassell
2019-04-26Fix some broken interpreter testsAlasdair Armstrong
2019-04-26More constructor monomorphisation supportBrian Campbell
2019-04-25Update coq read_mem/write_mem.Prashanth Mundkur
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-25Update prelude in mono testsBrian 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-19Coq: more robust handling of unknown constraintsBrian Campbell
2019-04-18Parameterise memory read/write primitives by address lengthJon French
2019-04-17Add interpreter annots to vector_dec.Prashanth Mundkur
2019-04-17Coq: support pure loops with termination measuresBrian Campbell
2019-04-17now without memory leaksJon French
2019-04-17add unimplemented C platform definitions for platform_read_mem etcJon French
2019-04-17Merge pull request #42 from crabtw/sail2Robert Norton
2019-04-17Add base64 package constraintJyun-Yan You
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-11 06:02:12 +0000