| Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
pretty print lret effects into lem
|
|
just an id (hopefully fixes Christopher issue).
|
|
|
|
TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
|
|
|
|
|
|
|
|
Add type refinement to arm spec
|
|
constraints, breaking power.
Also improve reporting of contract constraints, but then turn them off :( to allow power to compile.
|
|
|
|
|
|
incorrect LMA values (since sail interpreter now translates PC addresses).
|
|
|
|
checker
|
|
|
|
|
|
Interp: trying to add some debugging to isolate bug
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
requires some clean up (currently one huge function).
|
|
|
|
decode/translate_address/exhaustive. (Was previously correct for full register reads)
|
|
Attempt to get correct behaviour wrt nextpC on instruction fetch exception (prob. still wrong).
|
|
|
|
fix bug in interp_to_value_helper
|
|
(although decode isn't pushed through yet).
Note: this will break all builds
|
|
then reconvert delayedPC
|
|
|
|
|
|
implementation for now and exceptions not properly handled.
|
|
|