summaryrefslogtreecommitdiff
path: root/lib
AgeCommit message (Expand)Author
2018-05-15Merge branch 'sail2' into mappingsJon French
2018-05-11Add snapshot of generated Isabelle theoriesThomas Bauereiss
2018-05-10Merge branch 'sail2' into mappingsJon French
2018-05-09Fix an issue with C compilationAlasdair Armstrong
2018-05-09Add tests for Isabelle->OCaml generation for CHERI and AArch64Thomas Bauereiss
2018-05-09Run ARM built-in tests for Lem backend (via OCaml)Thomas Bauereiss
2018-05-03Flow typing and l-expression changes for ASL parserAlasdair Armstrong
2018-05-03Work in progress on the coq backendBrian Campbell
2018-05-01it worksJon French
2018-04-24Add some explanations to free monad documentationThomas Bauereiss
2018-04-20Make building of Isabelle heap image optionalThomas Bauereiss
2018-04-19Fix minor typo.Prashanth Mundkur
2018-04-19more nuanced discussion of generating HOL4 and CoqPeter Sewell
2018-04-18Add generated PDF of documentation draft --- comments welcomeThomas Bauereiss
2018-04-18Add first draft of Isabelle library documentationThomas Bauereiss
2018-04-18Add a simple Hoare logic for sequential reasoning to the libraryThomas Bauereiss
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
2018-04-13Add a few more generated file to gitignoreBrian Campbell
2018-04-11Fix neq_range in flow.sailAlasdair Armstrong
2018-04-10Porting some minisail changes to sail2 branchAlasdair Armstrong
2018-04-06Add integer comparisons to overloads in flow typing libraryAlasdair Armstrong
2018-04-06Update sail.tex for wip latex outputAlasdair Armstrong
2018-04-05Fix precedence printing and update aarch64 specAlasdair Armstrong
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-04-03Added test cases for builtinsAlasdair Armstrong
2018-03-22Fix C compilation for CHERI and MIPSAlasdair Armstrong
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas Bauereiss
2018-03-14Add address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
2018-03-13Polymorphic option types now compile to CAlasdair Armstrong
2018-03-12ELF loading for C backendAlasdair Armstrong
2018-03-07Make union types consistent in the ASTAlasdair 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:29:23 +0000