summaryrefslogtreecommitdiff
path: root/src/InterpreterUtils.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-15 21:15:20 +0100
committerSon Ho2022-01-15 21:15:20 +0100
commit231c65c04c511db3c8f7f68cd5d37cdeeedfe809 (patch)
treefbf656ae97d6a00c21f344c6de9fc50e444d9089 /src/InterpreterUtils.ml
parent9711789ae50ddcf2d2f4181044ba4f5eeb139ec8 (diff)
Use the new collections
Diffstat (limited to '')
-rw-r--r--src/InterpreterUtils.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index fc86f1f5..971dc801 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -192,7 +192,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
check that the set of ended regions doesn't intersect the set of
regions used in the type (this is more general).
*)
-let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t)
+let symbolic_value_has_ended_regions (ended_regions : T.RegionId.Set.t)
(s : V.symbolic_value) : bool =
let regions = rty_regions s.V.sv_ty in
not (T.RegionId.Set.disjoint regions ended_regions)
@@ -202,7 +202,7 @@ let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t)
Note that this function is very general: it also checks wether
symbolic values contain already ended regions.
*)
-let bottom_in_value (ended_regions : T.RegionId.set_t) (v : V.typed_value) :
+let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
bool =
let obj =
object