summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
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
2017-11-07Add builtin for reversing endiannessThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
2017-11-03Fix ocaml test suiteAlasdair Armstrong
2017-10-31Improvements to register read tracing in ocaml backendAlasdair Armstrong
2017-10-27Fixed some ocaml backend related bugsAlasdair Armstrong
2017-10-26Fix a bug in Sail OCaml libraryAlasdair Armstrong
2017-10-26Updated ocaml backend so tracing instrumentation is optional.Alasdair Armstrong
2017-10-25Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-25Avoid name clash in generated LemBrian Campbell
2017-10-23Added support for better tracing in ocaml backendAlasdair Armstrong
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-18Fixes and updates to ocaml backend to compile aarch64_no_vectorAlasdair Armstrong
2017-10-18Mark more prelude functions externBrian Campbell
2017-10-13Name (bit)vector operations more explicitlyThomas Bauereiss
2017-10-13Add support for real numbers to Lem backendThomas Bauereiss
2017-09-29Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experimentsThomas Bauereiss
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
2017-09-29Move Isabelle libraryThomas Bauereiss
2017-09-26Added while-do and repeat-until loops to sail for translating ASLAlasdair Armstrong
2017-09-18Added additional utility functions in ast_utilAlasdair Armstrong
2017-09-14Fix some more test casesThomas Bauereiss
2017-09-07Add ocaml run-time and updates to sail for ocaml backendAlasdair Armstrong
2017-08-29Make Lem export of CHERI(-256) typecheckThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:08:44 +0000