| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-06-06 | Some additional fixes to C backend. Re-enable primitive optimizations. | Alasdair Armstrong | |
| Also add an additional -Oz3 flag that uses z3 to optimize some additional types. This is currently very experimental and doesn't fully work yet. | |||
| 2018-05-23 | A couple of missing >= 0 constraints on vector handling functions | Brian Campbell | |
| 2018-05-09 | Run ARM built-in tests for Lem backend (via OCaml) | Thomas Bauereiss | |
| 2018-04-03 | Added test cases for builtins | Alasdair Armstrong | |
| Added library for simple integer arithmetic functions in lib/arith.sail WIP TeX file for formatting latex output included in lib/sail.tex Fixes for bugs in sail_lib | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |