| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-09-25 | tests: Move copy-pasted code into a shared helper .sh | Alex Richardson | |
| Also fix a few shellcheck warnings related to printf while doing so. | |||
| 2019-01-21 | Pass Lem library path to Isabelle | Thomas Bauereiss | |
| 2019-01-21 | Don't require manual set up of Isabelle session directories | Thomas Bauereiss | |
| Since Isabelle 2018, specifying the same directory both on the command line and persistently in the user's ROOTS file is allowed, so we don't have to choose between one or the other any more. | |||
| 2018-07-11 | Update CHERI code extraction from Isabelle | Thomas Bauereiss | |
| Also use zero-initialised memory. Apparently some tests access unitialised memory, and the default behaviour of the Lem shallow embedding is to fail in this case. | |||
| 2018-07-09 | Update CHERI code generation from Isabelle | Thomas Bauereiss | |
| 2018-07-09 | Simplify treating of undefined_bool in Lem library | Thomas Bauereiss | |
| Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list. | |||
| 2018-05-17 | Clean out old sequential files | Brian Campbell | |
| 2018-05-17 | Fix Isabelle->OCaml wrapper | Thomas Bauereiss | |
| 2018-05-11 | Add Isabelle code generation for sequential CHERI model | Thomas Bauereiss | |
| 2018-05-09 | Adapt Isabelle code generation to Byte_sequence changes | Thomas Bauereiss | |
| 2018-05-09 | Add tests for Isabelle->OCaml generation for CHERI and AArch64 | Thomas Bauereiss | |
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |