summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-28User defined overloaded operatorsAlasdair Armstrong
2017-06-28Improvements to implicit type castingAlasdair Armstrong
2017-06-27More features in bi-directional typecheckerAlasdair Armstrong
2017-06-26Added register fields for l-values expressions, and enumerationsAlasdair Armstrong
2017-06-24Added implicit castingAlasdair Armstrong
2017-06-23Added support for overloaded operatorsAlasdair Armstrong
2017-06-23Support for more sail constructsAlasdair Armstrong
2017-06-22Added basic if statements without flow constraintsAlasdair Armstrong
2017-06-22Added vector subrange support, and testsAlasdair Armstrong
2017-06-22Added support for vector append and indexingAlasdair Armstrong
2017-06-22Can now typecheck register declarations and assignmentsAlasdair Armstrong
2017-06-22Added support for bitvectorsAlasdair Armstrong
2017-06-16Some small changes to bi-directional checkerAlasdair Armstrong
2017-06-15Added support for default order declarations.Alasdair Armstrong
2017-06-15Prototype Bi-directional type checking algorithm for sailAlasdair Armstrong
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
2017-05-02docPeter Sewell
2017-04-27avoid out of bounds indicies in cheri128 decompression functions.Robert Norton
2017-04-27also trace memory writes.Robert Norton
2017-04-27remove undefined value from cheri 128 spec. The ocaml shallow embedding canno...Robert Norton
2017-04-27fix incorrect vector index in cheri128 spec. Should ideally have been caught ...Robert Norton
2017-04-27fix cheri128 model referring to wrong registers and not capreg printing.Robert Norton
2017-04-27need brackets around try ... with expression.Robert Norton
2017-04-27add command line argument for setting undef values to all zero or all one. So...Robert Norton
2017-04-27reverse endianness of data when writing UART. Altera jtag uart is little-endi...Robert Norton
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 20:19:46 +0000