diff options
| author | Alasdair | 2019-05-13 23:32:11 +0100 |
|---|---|---|
| committer | Alasdair | 2019-05-13 23:32:11 +0100 |
| commit | 7626da55ce21cb885da4af70cd5724ca33a00b65 (patch) | |
| tree | d52919ab0ce2b1b5ca71c17f6d9c15bc39a9018c /src/interpreter.ml | |
| parent | 3677cfc13e19efe650488a3a25917324bd6ccef7 (diff) | |
| parent | 7257b23239a3f8d6a45f973b9d953b31772abe06 (diff) | |
Merge branch 'sail2' into smt_experiments
Diffstat (limited to 'src/interpreter.ml')
| -rw-r--r-- | src/interpreter.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/interpreter.ml b/src/interpreter.ml index 9acfeb26..db4f45f6 100644 --- a/src/interpreter.ml +++ b/src/interpreter.ml @@ -388,14 +388,14 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = read_reg regname >>= fun v -> return (exp_of_value v) | "read_mem" -> begin match evaluated with - | [rk; addr; len] -> + | [rk; addrsize; addr; len] -> read_mem (value_of_exp rk) (value_of_exp addr) (value_of_exp len) >>= fun v -> return (exp_of_value v) | _ -> fail "Wrong number of parameters to read_mem intrinsic" end | "write_mem_ea" -> begin match evaluated with - | [wk; addr; len] -> + | [wk; addrsize; addr; len] -> write_ea (value_of_exp wk) (value_of_exp addr) (value_of_exp len) >> wrap unit_exp | _ -> fail "Wrong number of parameters to write_ea intrinsic" @@ -409,7 +409,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) = end | "write_mem" -> begin match evaluated with - | [wk; addr; len; v] -> + | [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)) | _ -> fail "Wrong number of parameters to write_memv intrinsic" |