diff options
Diffstat (limited to 'common/Determinism.v')
| -rw-r--r-- | common/Determinism.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/common/Determinism.v b/common/Determinism.v index a813dd92..7fa01c2d 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -42,18 +42,18 @@ Require Import Behaviors. CoInductive world: Type := World (io: string -> list eventval -> option (eventval * world)) - (vload: memory_chunk -> ident -> int -> option (eventval * world)) - (vstore: memory_chunk -> ident -> int -> eventval -> option world). + (vload: memory_chunk -> ident -> ptrofs -> option (eventval * world)) + (vstore: memory_chunk -> ident -> ptrofs -> eventval -> option world). Definition nextworld_io (w: world) (evname: string) (evargs: list eventval) : option (eventval * world) := match w with World io vl vs => io evname evargs end. -Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) : +Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: ptrofs) : option (eventval * world) := match w with World io vl vs => vl chunk id ofs end. -Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) (v: eventval): +Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: ptrofs) (v: eventval): option world := match w with World io vl vs => vs chunk id ofs v end. |