diff --git a/tests/misc/bts1347.ml b/tests/misc/bts1347.ml index d7196ae5940a4fc1316bb328207cfdc4044e0803..ea417ba7710a999aa54681cf88770f622473b46f 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 402616dac4b83282d03f51ba07270078fd889677..5bf2774757d4402519d82ae1590fef2b179ca7ea 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 5a4231067b4463e3e5e1647b6eb1acdb39d278fc..308f4e84faac142bf859f27f65f499b5d4aa70fc 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 1e06b3584e36988ad6886ac41835386b5d0a74f2..44c8841ce20ff11081d17df4ce27678a661ef8a5 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 f7eb9feb2d4d8f570fac58f298a24a3cef441a36..09aed9706740778962c1c6659d66b083a4214ed1 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) ;;