summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-13 21:56:36 +0100
committerSon Ho2022-01-13 21:56:36 +0100
commit0658739222a23474c5453eb32f282587ae8eb95e (patch)
tree0695538e1d6eab64ca16fcae97c0395d307082c1 /src/Interpreter.ml
parent19783cea9664e5ac0b14419b4aa961716010aafb (diff)
Update the projectors to ignore values when they don't contain regions
of interest
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index f38cb66e..d85c4bf8 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -77,7 +77,9 @@ module Test = struct
(* Add the avalues to the abstractions and insert them in the context *)
let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
(* Project over the values - we use *loan* projectors, as explained above *)
- let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in
+ let avalues =
+ List.map (mk_aproj_loans_from_symbolic_value abs.regions) input_svs
+ in
(* Insert the avalues in the abstraction *)
let abs = { abs with avalues } in
(* Insert the abstraction in the context *)