diff options
| author | Alasdair | 2020-03-25 16:09:00 +0000 |
|---|---|---|
| committer | Alasdair | 2020-03-25 16:09:00 +0000 |
| commit | f91839f0e8a625ea2f0b106a22a7095718a3e461 (patch) | |
| tree | 492fa5aed964995149c65fc433083b2652810210 /src/interpreter.ml | |
| parent | fe87bb2c265fde375a1977f8e38c0b1e9162872a (diff) | |
Fix a typo in write_mem for the interpreter
Diffstat (limited to 'src/interpreter.ml')
| -rw-r--r-- | src/interpreter.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 4c048c09..a30e90bc 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -408,7 +408,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = | "write_mem" -> begin match evaluated with | [wk; addrsize; addr; len; v] -> - write_mem (value_of_exp wk) (value_of_exp v) (value_of_exp len) (value_of_exp v) >>= fun b -> return (exp_of_value (V_bool b)) + write_mem (value_of_exp wk) (value_of_exp addr) (value_of_exp len) (value_of_exp v) >>= fun b -> return (exp_of_value (V_bool b)) | _ -> fail "Wrong number of parameters to write_memv intrinsic" end |