summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2018-03-14Fix toplevel pattern compilationAlasdair Armstrong
2018-03-14Machine words extract/update operations arguments are the other way aroundBrian Campbell
2018-03-14Remove unnecessary size_itself_int uses in guards (for Lem)Brian Campbell
2018-03-14Fix compilation for OCaml 4.02Thomas Bauereiss
2018-03-14Fix Lem generation for CHERI-MIPS and Aarch64Thomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add rewriting step for moving execute clauses into auxiliary functionsThomas Bauereiss
2018-03-14Disallow impure global let bindingsThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
2018-03-14fix riscv build: missing eq_bit implementation.Robert Norton
2018-03-13Polymorphic option types now compile to CAlasdair Armstrong
2018-03-13Add test for mutual recursion and monomorphisationBrian Campbell
2018-03-13Support a few more set constraints in monoBrian Campbell
2018-03-13Merge funcls for Lem output, making it suitable for testing with OCamlBrian Campbell
2018-03-12ELF loading for C backendAlasdair Armstrong
2018-03-12lem_interp: expose disable color flag in Printing_functions interfaceJon French
2018-03-09Specialise constructors for polymorphic unionsAlasdair Armstrong
2018-03-08rename mips_new_tc to mipsRobert Norton
2018-03-07Make union types consistent in the ASTAlasdair Armstrong
2018-03-06finish port of cheri128 spec. to sail2.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-02Fix off-by-one error in OCaml for loop compilationAlasdair Armstrong
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 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-26work around linksem crashing when trying to print an elf file where entry_poi...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-23Fix some bugs in C compilationAlasdair Armstrong
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-22More updates to C backendAlasdair Armstrong
2018-02-22Curtail at more false assertionsBrian Campbell
2018-02-22Merge branch 'sail2' of github.com:rems-project/sail into sail2Robert Norton
2018-02-22wipRobert Norton
2018-02-22Some Lem/OCaml compatibility fixesBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:09:07 +0000