| 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
|
|
kcc.base is non-zero.
|
|
|
|
constraints, breaking power.
Also improve reporting of contract constraints, but then turn them off :( to allow power to compile.
|
|
stores an absolute cursor instead of offset relative to base as a uarch optimisation. This is now part of the ISA and there is a test for it.
|
|
no functional change.
|
|
little loose at the moment (does not specify what to do with deprecated permission bits).
|
|
this is required for copying data via (untagged) capabilities.
|
|
|
|
|
|
|
|
incorrect LMA values (since sail interpreter now translates PC addresses).
|
|
want indexing of pfn to be reset to 23..0). Kathy to investigate why this was not caught by type checker.
|
|
|
|
halt instructions decode statements are a special case of mtc0 so clauses must appear first.
|
|
checker
|
|
|
|
in comments. No functional change.
|
|
|
|
|
|
|
|
|
|
Interp: trying to add some debugging to isolate bug
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
mips/cheri model.
|
|
|
|
|
|
|
|
to non-existent mips.sail in top level README.
|
|
|
|
|
