summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2018-03-01fix typo in flow.sailRobert Norton
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-23Fix some bugs in C compilationAlasdair Armstrong
2018-02-22More updates to C backendAlasdair Armstrong
2018-02-21Can now compile aarch64/no_vector into CAlasdair Armstrong
2018-02-19Have generic vectors working in C backendAlasdair Armstrong
2018-02-16Add __TakeColdReset function to aarch64_no_vectorAlasdair Armstrong
2018-02-16Add alternative definitions of aarch64 functions for monomorphisationBrian Campbell
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-02-15List support in C backendAlasdair Armstrong
2018-02-14Another mono rewrite for aarch64Brian Campbell
2018-02-13Support for large bitvector literals in C backendAlasdair Armstrong
2018-02-08Add (most of) the bitvector cast insertion transformationBrian Campbell
2018-02-06Compile union types in C backendAlasdair Armstrong
2018-02-02Add arithmetic shift right for aarch64 monoBrian Campbell
2018-02-01More work on C compilationAlasdair Armstrong
2018-01-31More updates to C backend - matching and tuplesAlasdair Armstrong
2018-01-31Add wrappers around Lem operators using bitvector type classThomas Bauereiss
2018-01-31Split base definitions of Lem monads and further built-ins (e.g. loop combina...Thomas Bauereiss
2018-01-30Fix failing Lem testsAlasdair Armstrong
2018-01-29Sync mono rewrites definitions with libraryBrian Campbell
2018-01-29Shaked removing generation of now-uncessary uint dependencyPeter Sewell
2018-01-26Fixed loading ARM elf filesAlasdair Armstrong
2018-01-26One more mono rewriteBrian Campbell
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2018-01-22Update and fix test suiteAlasdair Armstrong
2018-01-19Update monomorphisation for sail2Brian Campbell
2018-01-18Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-18Modified ocaml backend to use ocamlfind for linksem and lemAlasdair Armstrong
2018-01-16Another useful monomorphisation rewriteBrian Campbell
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2018-01-09More monomorphisation rewrites for aarch64Brian Campbell
2018-01-09Add some optional experimental rewrites to help with monomorphisationBrian Campbell
2017-12-14An experimental version of sail without bitvector start indexes.Alasdair Armstrong
2017-12-14Merge remote-tracking branch 'origin/experiments' into interactiveAlasdair Armstrong
2017-12-13Cleanup code by fixing compiler warnings, and fix ocaml compilationAlasdair Armstrong
2017-12-12Add a few helper functions for bit listsThomas Bauereiss
2017-12-07Support monomorphisation with set constrained integersBrian Campbell
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
2017-11-28Small update to trivial sizeof rewrites so we can handle all cases inAlasdair Armstrong
2017-11-27Compile assertions into OCamlAlasdair Armstrong
2017-11-21Expose entry point in elf_loader for Sail modelAlasdair Armstrong
2017-11-15Additional test case for OCaml backendAlasdair Armstrong
2017-11-15Simplify flow typing code in typecheckerAlasdair Armstrong
2017-11-10Fixed ocaml backend so it correctly compiles registers passed by name.Alasdair Armstrong
2017-11-08Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into ex...Alasdair Armstrong