summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-07-20add new CNEXEQ instruction.Robert Norton
2017-07-19split library tests into separate files to avoid risk of sail compiler stack ...Robert Norton
2017-07-19borrow some of aa's bash code to convert library test suite output to junit ...Robert Norton
2017-07-06Tests for (almost) all sail builtins. Many interesting things discovered. Lib...Robert Norton
2017-07-06fix off by one in type of add_vec builtin function. There are many more dubio...Robert Norton
2017-07-06fix interpreter version of get_min/max_representable which similarly broken t...Robert Norton
2017-07-06fix interpreter lteq/gteq for range/vec.Robert Norton
2017-07-06fix interpreter version of != which was broken for vector/range comparisons.Robert Norton
2017-07-06substitute all uses of mod_big_int and div_big_int for Z.rem and Z.div which ...Robert Norton
2017-07-06implement abs function correctly for ocaml shallow embedding.Robert Norton
2017-07-06fix dodgy get_min/max_representable functions. Looks like an attempt at optim...Robert Norton
2017-07-04further testing of sail library.Robert Norton
2017-07-04change to cgettype -- returns -1 if not sealed instead of 0.Robert Norton
2017-07-03Update to copytype and ccseal -- now use belt and braces approach when handli...Robert Norton
2017-06-30add more tests for sail library. Can't compile entire file due to sail perfor...Robert Norton
2017-06-29beginnings of a sail library test suite.Robert Norton
2017-06-22fix three different copies of the hardware_quot function to do proper trucati...Robert Norton
2017-06-22add a 'print' built-in function handy for writing sail tests.Robert Norton
2017-06-22fix a typo spotted in CPtrCmp instruction -- CLEU was using signed comparison...Robert Norton
2017-06-22revised ccopytype with check for offset being in bounds and clearing tag inst...Robert Norton
2017-06-16prefer arithmetic on integers followed by cast to bit[64] in CCopyType.Robert Norton
2017-06-16remove unnecessary local variable definitions copy and pasted from cbuildcap.Robert Norton
2017-06-16fix previous commit so that it builds.Robert Norton
2017-06-16implement new CBuildCap and CCopyType instrucitons for ISAv6.Robert Norton
2017-06-14Add a work-in-progress version of sail_values.lemBrian Campbell
2017-06-13Add Makefile and ROOT for Isabelle libraryThomas Bauereiss
2017-06-05Attempt to make Lem-prettyprinting of function clauses more robustThomas Bauereiss
2017-06-05Fix pretty-printing of function clauses with wildcards for LemThomas Bauereiss
2017-06-02Add tag memory to Lem shallow embeddingThomas Bauereiss
2017-05-28fixed exmemShaked Flur
2017-05-26fix run_with builds after build_context gained an extra argument.Robert Norton
2017-05-26add cmovz and cmovn conditional capability move instructions new in ISAv6.Robert Norton
2017-05-26Update ctoptr instruction to check that all of ct is within bounds of cb and ...Robert Norton
2017-05-26in ISAv6 cjr and cjalr are permitted on local capabilities.Robert Norton
2017-05-26add support for the new ccall selector 1 implementation that directly unseals...Robert Norton
2017-05-24fixed missing _tag bitsShaked Flur
2017-05-24Merge branch 'master' of bitbucket.org:Peter_Sewell/sailShaked Flur
2017-05-24added the exmem effect for AArch64 store-exclusiveShaked Flur
2017-05-24Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from dat...Robert Norton
2017-05-24it turns out that Zarith has a divide function which does truncation towards ...Robert Norton
2017-05-10Fix type error in CGetLenThomas Bauereiss
2017-05-10Further to Thomas's commit remove the duplicate declarations of max_otype and...Robert Norton
2017-05-10Add stubs for TAGwThomas Bauereiss
2017-05-10Comment out duplicate definitions in cheri_types.sailThomas Bauereiss
2017-05-10Build Cheri_embed_types.thy together with Cheri_embed_sequential.thyThomas Bauereiss
2017-05-08add make rules to (attempt to) build arm and power ml.Robert Norton
2017-05-08add target for building ocaml shallow embed for arm.Robert Norton
2017-05-08add some missing things in sail_values and make big_int version the default f...Robert Norton
2017-05-08add error messages for unhandled pattern match nodes in ocaml pretty printer.Robert Norton
2017-05-08put failwith in brackets to avoid parse error.Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 09:31:42 +0000