diff options
Diffstat (limited to 'cfrontend/Cexec.v')
| -rw-r--r-- | cfrontend/Cexec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 36a62a8..79dd26f 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -205,7 +205,7 @@ Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block : option (world * trace * mem) := if block_is_volatile ge b then do id <- Genv.invert_symbol ge b; - do ev <- eventval_of_val v (type_of_chunk chunk); + do ev <- eventval_of_val (Val.load_result chunk v) (type_of_chunk chunk); do w' <- nextworld_vstore w chunk id ofs ev; Some(w', Event_vstore chunk id ofs ev :: nil, m) else |