[kernel] Use the new modules in tests instead of deprecated Db.Properties

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

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)
 

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;

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

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)
 ;;