| Age | Commit message (Collapse) | Author |
|---|
|
|
|
(still need to sort out some string stuff, though)
|
|
to match new constraints in prelude
|
|
|
|
(necessary for backends where they're different)
Coq uint/sint and related fixes
|
|
|
|
|
|
|
|
|
|
|
|
(The last bit is to declare type aliases as Type so that Coq uses the
type scope for notation, so * is prod, not multiplication).
|
|
(also another error reporting improvement)
|
|
|
|
Plus
- Complete solver support for inequalities
- Reduce exponentials in solver
|
|
|
|
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
|
|
|
|
|
