summaryrefslogtreecommitdiff
path: root/src/gen_lib/sail_values.lem
AgeCommit message (Expand)Author
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-05Add generic prelude library that pulls in various basic sailAlasdair Armstrong
2018-03-22Tune Lem pretty-printingThomas Bauereiss
2018-03-14Make partiality more explicit in library functions of Lem shallow embeddingThomas 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-27Lem/OCaml compatibility fixesBrian Campbell
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-31Add wrappers around Lem operators using bitvector type classThomas Bauereiss
2018-01-22Update Lem shallow embedding to Sail2Thomas Bauereiss
2017-12-12Add a few helper functions for bit listsThomas Bauereiss
2017-12-06Make AST after rewriting for Lem backend type-checkableThomas Bauereiss
2017-11-07Add builtin for reversing endiannessThomas Bauereiss
2017-11-07Declare prelude functions as externThomas Bauereiss
2017-10-23Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-10-19Make some potentially non-terminating library functions terminateThomas Bauereiss
2017-10-18Merge branch 'experiments' of Peter_Sewell/sail into mono-experimentsBrian Campbell
2017-10-13Make Sail_values.repeat total, and remove duplicateBrian Campbell
2017-10-13Name (bit)vector operations more explicitlyThomas Bauereiss
2017-10-13Add support for real numbers to Lem backendThomas Bauereiss
2017-10-02Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-09-29Some more refactoring of Sail libraryThomas Bauereiss
2017-09-04Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-exper...Brian Campbell
2017-09-03added RISC-V strong-acquire/releaseShaked Flur
2017-08-29Make Lem export of CHERI(-256) typecheckThomas Bauereiss
2017-08-28Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into mono-exper...Brian Campbell
2017-08-24Begin refactoring Sail libraryThomas Bauereiss
2017-08-21Merge branch 'experiments' into mono-experimentsBrian Campbell
2017-08-18Correct indexing and equality for bitvectorsBrian Campbell
2017-08-18Fixed a bug where sizeof re-writing fail for aliased type argumentsAlasdair Armstrong
2017-08-17Add support for register types other than bitvector to state monadThomas Bauereiss
2017-08-17Merge remote-tracking branch 'origin' into mono-experimentsBrian Campbell
2017-08-16Eta-expansion in sail_values to make OCaml happyBrian Campbell
2017-08-14Merge remote-tracking branch 'origin/master' into experimentsAlasdair Armstrong
2017-08-12Resolve ambiguity between negation of integers and boolsThomas Bauereiss
2017-08-10Add support for early return to Lem backendThomas Bauereiss
2017-08-08Glue together Sail prelude and Lem libraryThomas Bauereiss
2017-08-01Remove some hardcoded calls to obsolete Lem library functionsThomas Bauereiss
2017-07-26Merge remote-tracking branch 'origin/master' into sail_new_tcAlasdair Armstrong
2017-06-22fix three different copies of the hardware_quot function to do proper trucati...Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:21:28 +0000