| Age | Commit message (Collapse) | Author |
|
unknown conditions.
Does not merge if one path has resulted in an exit
|
|
|
|
|
|
theorem provers, use structural (in)equality for Isabelle and HOL for literals and values
|
|
being very power-specific.
Note: slight interface change to instruction_extractor
|
|
|
|
Also fix type checker bug in not reporting modifications to parameter values
|
|
increasing while supporting inc and dec views to the interpreter and in printing
Fix bugs exposed by running idlarm several instructions (after fixing above)
|
|
Split out specification specific memory and external functions
Reduce the presence of big_int
Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction
Also some bug fixes exposed by above and running ARM second instruction
|
|
and I *think* that I'm making vectors of unknowns in all the necessary places now.
|
|
|
|
|