summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
2018-02-22Point merlin at pprint buildBrian Campbell
2018-02-21Can now compile aarch64/no_vector into CAlasdair Armstrong
2018-02-21Implement more builtins in constant propagationBrian Campbell
2018-02-21Cut out dead if branches according to the type environment during monoBrian Campbell
2018-02-21Create an update_field function for each field in a bitfield definitionAlasdair Armstrong
2018-02-21Have aarch64/no_vector compiling to CAlasdair Armstrong
2018-02-21clean LICENCEPeter Sewell
2018-02-20Remove temporary debugging messageBrian Campbell
2018-02-20Bump up case split limit for nowBrian Campbell
2018-02-20Simplifying nexp division, since the type checker can introduce itBrian Campbell
2018-02-20Report unsupported nexps properly in Lem backendBrian Campbell
2018-02-20Rework atom-to-itself transformation to check for equivalent size nexpsBrian Campbell
2018-02-20Look for alternative size annotations when pretty printing LemBrian Campbell
2018-02-20Allow overlapping bitfield field namesAlasdair Armstrong
2018-02-19Have generic vectors working in C backendAlasdair Armstrong
2018-02-17Merge master branch into sail2 for OCaml 4.06 compatibilityThomas Bauereiss
2018-02-16Avoid nested explicit type annotationsThomas Bauereiss
2018-02-16Don't generate undefined functions for generated register typesThomas Bauereiss
2018-02-16Add __TakeColdReset function to aarch64_no_vectorAlasdair Armstrong
2018-02-16Can now compile aarch64/duopod to CAlasdair Armstrong
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-02-15C backend can now handle record literals and record update syntax correctlyAlasdair Armstrong
2018-02-15Update duopod spec so it has no address translationAlasdair Armstrong
2018-02-15List support in C backendAlasdair Armstrong
2018-02-14Another mono rewrite for aarch64Brian Campbell
2018-02-14Support monorphisation analysis of bitvectors inside existentialsBrian Campbell
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:55:35 +0000