From ed3c0d14f34b42761e1ecfef401a34525e6ac412 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 13 Oct 2022 14:27:44 +0200
Subject: [PATCH] [kernel] Use the new modules in tests instead of deprecated
Db.Properties
---
tests/misc/bts1347.ml | 2 +-
tests/pdg/dyn_dpds.ml | 4 ++--
tests/scope/bts971.ml | 4 ++--
tests/scope/zones.ml | 4 ++--
tests/slicing/libSelect.ml | 4 ++--
5 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml
index d7196ae5940..ea417ba7710 100644
--- a/tests/misc/bts1347.ml
+++ b/tests/misc/bts1347.ml
@@ -18,7 +18,7 @@ let run () =
[]
in
let s = Kernel_function.find_return kf in
- let ca = !Db.Properties.Interp.code_annot kf s "assert 32.5>=10.;" in
+ let ca = Logic_parse_string.code_annot kf s "assert 32.5>=10.;" in
Annotations.add_code_annot emitter ~kf s ca;
let ip = Property.ip_of_code_annot_single kf s ca in
Property_status.emit emitter ~hyps ip Property_status.True
diff --git a/tests/pdg/dyn_dpds.ml b/tests/pdg/dyn_dpds.ml
index 402616dac4b..5bf2774757d 100644
--- a/tests/pdg/dyn_dpds.ml
+++ b/tests/pdg/dyn_dpds.ml
@@ -6,8 +6,8 @@ zgrviewer tests/pdg/dyn_dpds_2.dot ;
*)
let get_zones str_data (stmt, kf) =
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let exp = Cil.new_exp ~loc:Cil_datatype.Location.unknown (Cil_types.Lval lval) in
Eva.Results.(before stmt |> expr_deps exp)
diff --git a/tests/scope/bts971.ml b/tests/scope/bts971.ml
index 5a4231067b4..308f4e84faa 100644
--- a/tests/scope/bts971.ml
+++ b/tests/scope/bts971.ml
@@ -8,8 +8,8 @@ let find_pp kf_name =
let compute_and_print pp str_data =
let stmt, kf = pp in
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let defs = Scope.Defs.get_defs kf stmt lval in
Format.printf "* @[<v 2>Defs for (%s) at current program point=@[<v 2>@."
str_data;
diff --git a/tests/scope/zones.ml b/tests/scope/zones.ml
index 1e06b3584e3..44c8841ce20 100644
--- a/tests/scope/zones.ml
+++ b/tests/scope/zones.ml
@@ -35,8 +35,8 @@ let find_label kf_name lab_name =
let compute_and_print pp str_data =
let stmt, kf = pp in
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let (_used_stmts, zones) = Scope.Zones.build_zones kf stmt lval in
Format.printf "Zones for %s at current program point =@.%a\n@\n"
str_data Scope.Zones.pretty_zones zones
diff --git a/tests/slicing/libSelect.ml b/tests/slicing/libSelect.ml
index f7eb9feb2d4..09aed970674 100644
--- a/tests/slicing/libSelect.ml
+++ b/tests/slicing/libSelect.ml
@@ -74,8 +74,8 @@ let get_stmt sid = fst (Kernel_function.find_from_sid sid)
(** build the [zone] which represents [data] before [kinst] *)
let get_zones str_data (stmt, kf) =
- let lval_term = !Db.Properties.Interp.term_lval kf str_data in
- let lval = !Db.Properties.Interp.term_lval_to_lval ~result:None lval_term in
+ let lval_term = Logic_parse_string.term_lval kf str_data in
+ let lval = Logic_to_c.term_lval_to_lval lval_term in
let loc = Eva.Results.(before stmt |> eval_address lval |> as_location) in
Locations.(enumerate_valid_bits Read loc)
;;
--
GitLab