summaryrefslogtreecommitdiff
path: root/src/ValuesUtils.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-18 23:03:55 +0100
committerSon Ho2022-01-18 23:03:55 +0100
commitc0f230dc6c331e9eb120900e8c31a03e1f5ab476 (patch)
tree16ff97c6af5e85baab2e7f1af5456bd2854e057b /src/ValuesUtils.ml
parentcdef093fedaadcc5694cb9f7d63a4bf9814d5573 (diff)
Remove ty_has_regions and use ty_has_borrows instead
Diffstat (limited to 'src/ValuesUtils.ml')
-rw-r--r--src/ValuesUtils.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index 4555fd50..f3876f53 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -2,6 +2,7 @@ open Utils
open TypesUtils
open Types
open Values
+module TA = TypesAnalysis
exception FoundSymbolicValue of symbolic_value
(** Utility exception *)
@@ -88,8 +89,8 @@ let outer_loans_in_value (v : typed_value) : bool =
false
with Found -> true
-let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option
- =
+let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
+ (v : typed_value) : symbolic_value option =
(* The visitor *)
let obj =
object
@@ -97,7 +98,7 @@ let find_first_primitively_copyable_sv (v : typed_value) : symbolic_value option
method! visit_Symbolic _ sv =
let ty = sv.sv_ty in
- if ty_is_primitively_copyable ty && ty_has_regions ty then
+ if ty_is_primitively_copyable ty && ty_has_borrows type_infos ty then
raise (FoundSymbolicValue sv)
else ()
end