diff options
author | Son Ho | 2022-01-27 23:35:35 +0100 |
---|---|---|
committer | Son Ho | 2022-01-27 23:35:35 +0100 |
commit | 9fe5e13657ff1f3bdc376302cfa6197252c47a01 (patch) | |
tree | 79668263212bc2a9ecb685d6352263a777cea539 /src/InterpreterExpressions.ml | |
parent | 7e53ab2fd9162e2d85895ad1173f620c609a1c38 (diff) |
Rename the meta-places to [mplace] and update some comments
Diffstat (limited to '')
-rw-r--r-- | src/InterpreterExpressions.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml index 356bae2d..34bfd574 100644 --- a/src/InterpreterExpressions.ml +++ b/src/InterpreterExpressions.ml @@ -40,7 +40,8 @@ let expand_primitively_copyable_at_place (config : C.config) | None -> cf ctx | Some sv -> let cc = - expand_symbolic_value_no_branching config sv (Some (S.mk_place p ctx)) + expand_symbolic_value_no_branching config sv + (Some (S.mk_mplace p ctx)) in comp cc expand cf ctx in @@ -496,7 +497,7 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place) let allow_branching = true in let cc = expand_symbolic_value config allow_branching sv - (Some (S.mk_place p ctx)) + (Some (S.mk_mplace p ctx)) in (* This time the value is concrete: reevaluate *) comp cc (eval_rvalue_discriminant_concrete config p) cf ctx |