summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-06Add missing checks for permit_load and permit_store in capability load/store ...Robert Norton
2018-03-06Check tag of pcc in TranslatePC. This could happen after an ERET with untagge...Robert Norton
2018-03-06overload shift operators so they can be used with integer shifts in cheri128 ...Robert Norton
2018-03-06finish port of cheri128 spec. to sail2.Robert Norton
2018-03-06add atom versions of val declaration for min and max.Robert Norton
2018-03-05Fix specialisation pass to handle polymorphic substitutionsAlasdair Armstrong
2018-03-05Add Print outcome to prompt monad for debugging and tracingThomas Bauereiss
2018-03-05Add support for undefined bit oracle to Lem shallow embeddingThomas Bauereiss
2018-03-02Use sail_lib.lem values in C backendAlasdair Armstrong
2018-03-02Fix a bug in rewriting of loops for Lem backendThomas Bauereiss
2018-03-02Add full aarch64_no_vector monomorphisation demoBrian Campbell
2018-03-02remove workaround for #8 now that it is fixed.Robert Norton
2018-03-02Fix off-by-one error in OCaml for loop compilationAlasdair Armstrong
2018-03-02work around bug in ocaml foreach generation -- end point not included in loop...Robert Norton
2018-03-02add a cp2_next_pc function to update cheri state in fde loop and a stub versi...Robert Norton
2018-03-02add space in cap dump format to match that expected by test framework.Robert Norton
2018-03-02cheri tests expect reserved permission bits to be initialised to one.Robert Norton
2018-03-01Cleanup intermediate bytecode representation in C backendAlasdair Armstrong
2018-03-01Add support for read_tag and write_tag in sail_lib.ml. and support for intial...Robert Norton
2018-03-01fix typo in flow.sailRobert Norton
2018-03-01cheri wip.Robert Norton
2018-03-01Fix polymorphic functions annotations in OCaml compilationAlasdair Armstrong
2018-02-28Add check for if a function is redefining a val-specAlasdair Armstrong
2018-02-28Use topological sorting for OCaml backendThomas Bauereiss
2018-02-27Fix some bugs in C compilation, and optimise struct updatesAlasdair Armstrong
2018-02-27Get MIPS translated to LemThomas Bauereiss
2018-02-27Make constant propagation of slicing more generalBrian Campbell
2018-02-27Lem/OCaml compatibility fixesBrian Campbell
2018-02-26Add some obvious optimisations to C backend.Alasdair Armstrong
2018-02-26Last of the aarch64_no_vector monomorphisation replacementsBrian Campbell
2018-02-26work around linksem crashing when trying to print an elf file where entry_poi...Robert Norton
2018-02-26working sail2 mips spec (passes BERI tests).Robert Norton
2018-02-26ADDU should sign extend 32-bit result.Robert Norton
2018-02-26workaround sail2 not liking type synonyms as arguments to constructors (see #2).Robert Norton
2018-02-26Fix SLTIU: note that immediate must be sign extended before unsigned comparison!Robert Norton
2018-02-26Fix missing case in pattern completeness checkAlasdair Armstrong
2018-02-26Rename some Isabelle theoriesThomas Bauereiss
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-24Fix C builtinsAlasdair Armstrong
2018-02-23Change links in README to point to githubAlasdair Armstrong
2018-02-23Fix some bugs in C compilationAlasdair Armstrong
2018-02-23Make mono test harness nicerBrian Campbell
2018-02-23Allow guarded patterns rewrite to merge P_var patternsBrian Campbell
2018-02-23Merge branch 'sail2' of github.com:rems-project/sail into sail2Robert Norton
2018-02-23Some tidy up of sail library - use extract_num from Big_int to implement to_g...Robert Norton
2018-02-23Change monomorphisation tests to proper outputBrian Campbell
2018-02-23test commitPeter Sewell
2018-02-23Update more monomorphisation testsBrian Campbell
2018-02-22More updates to C backendAlasdair Armstrong
2018-02-22Curtail at more false assertionsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 10:11:13 +0000