Remove direct use of dstringt (and as_string)

We keep dstringt as an implementation detail.

Author: tautschnig

src/libcprover-cpp/verification_result.cpp

@@ -114,7 +114,7 @@ std::vector<std::string> verification_resultt::get_property_ids() const
   std::vector<std::string> result;
   for(const auto &props : _impl->get_properties())
   {
-    result.push_back(as_string(props.first));
+    result.push_back(id2string(props.first));
   }
   return result;
 }

unit/analyses/variable-sensitivity/abstract_environment/to_predicate.cpp

@@ -52,7 +52,7 @@ SCENARIO(
 
       auto type = signedbv_typet(32);
       auto val2 = make_constant(from_integer(2, type), env, ns);
-      auto x_name = symbol_exprt(dstringt("x"), type);
+      auto x_name = symbol_exprt("x", type);
 
       env.assign(x_name, val2, ns);
 
@@ -65,10 +65,10 @@ SCENARIO(
 
       auto type = signedbv_typet(32);
       auto val2 = make_constant(from_integer(2, type), env, ns);
-      auto x_name = symbol_exprt(dstringt("x"), type);
+      auto x_name = symbol_exprt("x", type);
 
       auto val3 = make_constant(from_integer(3, type), env, ns);
-      auto y_name = symbol_exprt(dstringt("y"), type);
+      auto y_name = symbol_exprt("y", type);
 
       env.assign(x_name, val2, ns);
       env.assign(y_name, val3, ns);

unit/analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp

@@ -25,7 +25,7 @@ SCENARIO(
   const typet type = signedbv_typet(32);
   const exprt val2 = from_integer(2, type);
 
-  const exprt x_name = symbol_exprt(dstringt("x"), type);
+  const exprt x_name = symbol_exprt("x", type);
 
   auto config = vsd_configt::constant_domain();
   config.context_tracking.data_dependency_context = false;

unit/analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp

@@ -24,9 +24,9 @@ SCENARIO(
 {
   const auto int_type = signedbv_typet(32);
   const auto ptr_type = pointer_typet(int_type, 32);
-  const auto val2_symbol = symbol_exprt(dstringt("val2"), int_type);
+  const auto val2_symbol = symbol_exprt("val2", int_type);
 
-  const auto x_name = symbol_exprt(dstringt("x"), int_type);
+  const auto x_name = symbol_exprt("x", int_type);
 
   auto config = vsd_configt::constant_domain();
   config.context_tracking.data_dependency_context = false;

unit/analyses/variable-sensitivity/interval_abstract_value/to_predicate.cpp

@@ -35,7 +35,7 @@ SCENARIO(
   const exprt val1 = from_integer(1, type);
   const exprt val2 = from_integer(2, type);
 
-  const exprt x_name = symbol_exprt(dstringt("x"), type);
+  const exprt x_name = symbol_exprt("x", type);
 
   auto config = vsd_configt::constant_domain();
   config.context_tracking.data_dependency_context = false;

unit/analyses/variable-sensitivity/value_expression_evaluation/assume.cpp

@@ -24,7 +24,7 @@
 #include <testing-utils/use_catch.h>
 
 exprt binary_expression(
-  dstringt const &exprId,
+  const irep_idt &exprId,
   const abstract_object_pointert &op1,
   const abstract_object_pointert &op2,
   abstract_environmentt &environment,
@@ -83,7 +83,7 @@ class assume_testert
   }
 
   void test_fn(
-    dstringt const &exprId,
+    const irep_idt &exprId,
     bool is_true,
     std::string const &test,
     std::string const &delimiter)

unit/analyses/variable-sensitivity/value_set_abstract_object/to_predicate.cpp

@@ -37,7 +37,7 @@ SCENARIO(
   const exprt interval_0_2 = constant_interval_exprt(val1, val2);
   const exprt interval_2_3 = constant_interval_exprt(val2, val3);
 
-  const exprt x_name = symbol_exprt(dstringt("x"), type);
+  const exprt x_name = symbol_exprt("x", type);
 
   auto config = vsd_configt::constant_domain();
   config.context_tracking.data_dependency_context = false;

unit/analyses/variable-sensitivity/value_set_pointer_abstract_object/to_predicate.cpp

@@ -32,10 +32,10 @@ SCENARIO(
 {
   const auto int_type = signedbv_typet(32);
   const auto ptr_type = pointer_typet(int_type, 32);
-  const auto val1_symbol = symbol_exprt(dstringt("val1"), int_type);
-  const auto val2_symbol = symbol_exprt(dstringt("val2"), int_type);
+  const auto val1_symbol = symbol_exprt("val1", int_type);
+  const auto val2_symbol = symbol_exprt("val2", int_type);
 
-  const auto x_name = symbol_exprt(dstringt("x"), int_type);
+  const auto x_name = symbol_exprt("x", int_type);
 
   auto config = vsd_configt::constant_domain();
   config.context_tracking.data_dependency_context = false;

unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp

@@ -590,7 +590,7 @@ std::shared_ptr<const value_set_abstract_objectt> add_as_value_set(
 
 void THEN_PREDICATE(const abstract_object_pointert &obj, const std::string &out)
 {
-  const auto x_name = symbol_exprt(dstringt("x"), obj->type());
+  const auto x_name = symbol_exprt("x", obj->type());
   auto pred = obj->to_predicate(x_name);
   THEN("predicate is " + out)
   {