summaryrefslogtreecommitdiff
path: root/src/gen_lib
AgeCommit message (Expand)Author
2018-05-09Fix printing of hex strings in LemThomas Bauereiss
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-09Support short-circuiting of Boolean expressions in LemThomas Bauereiss
2018-05-04Add back purely sequential Lem generationThomas Bauereiss
2018-04-20Have sign_extend in common Sail Lem library, use it and zero_extend inBrian Campbell
2018-04-18Add some lemmas about bitvectorsThomas Bauereiss
2018-04-18Move a few printing functions to sail_values.lemThomas Bauereiss
2018-04-18Move Lem shl_int, shr_int implementations from aarch64_extras to sail libBrian Campbell
2018-04-17Move some Lem library vector operations so that we also have mword versionsBrian Campbell
2018-04-05Cleanup repository by removing old and generated filesAlasdair Armstrong
2018-04-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Machine words extract/update operations arguments are the other way aroundBrian Campbell
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 address to Write_tag outcomeThomas Bauereiss
2018-03-14Use sets instead of lists for Lem nondeterminism monadThomas Bauereiss
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-02-27Get MIPS translated to LemThomas Bauereiss
2018-02-27Lem/OCaml compatibility fixesBrian Campbell
2018-02-26Rename some Isabelle theoriesThomas Bauereiss
2018-02-26Add/generate Isabelle lemmas about the monad liftingThomas Bauereiss
2018-02-22Some Lem/OCaml compatibility fixesBrian Campbell
2018-02-17Merge master branch into sail2 for OCaml 4.06 compatibilityThomas Bauereiss
2018-02-15Rebase state monad onto prompt monadThomas Bauereiss
2018-02-15Re-engineer prompt monad of Lem shallow embeddingThomas Bauereiss
2018-02-08replaced NIA_LR/CTR/register with NIA_indirect;Shaked Flur
2018-02-07Add some printing functions to Lem shallow embeddingThomas Bauereiss
2018-02-02Add M extension to RISCV. Slightly inelegant implementation for now but passi...Robert Norton
2018-01-31Export arithmetic shift right from Lem libraryThomas Bauereiss
2018-01-31Add Lem operator wrappers for bitlistsThomas Bauereiss
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-29Add rreg effect to _reg_deref in fix_val_specs rewriteThomas Bauereiss
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2018-01-12Merge remote-tracking branch 'origin/experiments' into sail2Alasdair Armstrong
2017-12-19Support user-defined exceptions in Lem shallow embeddingThomas Bauereiss
2017-12-14Merge remote-tracking branch 'origin/experiments' into interactiveAlasdair Armstrong
2017-12-13Use big_nums from LemAlasdair Armstrong
2017-12-12Add a few helper functions for bit listsThomas Bauereiss
2017-12-06Merge remote branch 'experiments' into experimentsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
2017-11-30Merge branch 'master' into experimentsAlasdair Armstrong
2017-11-07Add builtin for reversing endiannessThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
2017-11-02Merge branch 'experiments'Thomas Bauereiss
2017-11-02Fix translation of repeat-until loops to LemThomas Bauereiss
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 21:00:13 +0000