diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp_interface.lem | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem index 3d4b2e6d..f74a70db 100644 --- a/src/lem_interp/interp_interface.lem +++ b/src/lem_interp/interp_interface.lem @@ -52,10 +52,10 @@ val interp : interp_mode -> instruction_state -> outcome val interp_exhaustive : instruction_state -> list event +val rr_interp_exhaustive : instruction_state -> list event -> (outcome * (list event)) (* Like interp_exhaustive but will read registers; the outcome will only ever be a rreg request, done, or error *) + val mem_read_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory reads to compute the addressses in is*) val mem_write_analysis : instruction_state -> list event (*Should record all rreg events where the registers are involved in memory writes to compute the address (and value?, in a separate list?)*) -(*Questions : isync? any other special instructions that we need to inform the memory model etc. about - : let's look again at conditional memory instructions, based on the book *) |