diff options
| author | Alasdair Armstrong | 2019-05-21 17:31:13 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2019-05-21 17:41:52 +0100 |
| commit | 7b4bf2bd14cae99a4d8086a0b66d9875be1acbab (patch) | |
| tree | b0cb23843364c3154037b8ec494e8b96ddc765cd /src/jib | |
| parent | 9713d40546c732dab7ebd3d534267c696a0e84ed (diff) | |
SMT: Use a separate constructor for memory read variables
We want to ensure simplication can treat these separately so we
don't accidentally simplify away dependencies between reads and write
addresses.
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/jib_smt.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 7420707c..0d6f42fe 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1044,7 +1044,7 @@ let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp = let name = "R" ^ string_of_int !reads in [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk, smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))], - Var (name ^ "_ret") + Read_res name let excl_results = ref (-1) @@ -1626,7 +1626,7 @@ module Make_optimizer(S : Sequence) = struct | Some n -> Hashtbl.replace uses var (n + 1) | None -> Hashtbl.add uses var 1 end - | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () + | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> () | Fn (_, exps) | Ctor (_, exps) -> List.iter uses_in_exp exps | Ite (cond, t, e) -> |