| Age | Commit message (Collapse) | Author |
|---|
|
|
|
It can be proved almost entirely by symbolic execution (in <15s) _if_
the right definitions are in the compset. It took a lot of interactive
stumbling about to discover that LUPDATE was missing from the standard
list compset.
|
|
The proof now gets through simulation of the first instruction of the test.
|
|
|
|
|
|
|
|
|
|
terminal.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(involved some manual tinkering with gitignore, type_check, riscv)
|
|
wouldn't be legal in a pattern anyway
|
|
|
|
|
|
|
|
minstret CSR is explicitly written to.
|
|
|
|
|
|
This should fix the issue raised in commit 45554f
Adds a test loop_exception that tests throwing exceptions in loops, various looping constructs, and returning values from try/catch blocks. Also modified the test-suite to test C compiled output both with and without optimisations
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Plus test case, broken builtin name
|
|
|
|
|
|
- add existential unpacking for function arguments
- add mechanism for using properties for existentially typed top-level
values (useful for the typechecking tests)
- support for length_list and In in Coq constraint solving
|
|
Only single variable in places, only packed at literals and variables,
no unpacking
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
