Removed the dynamic_object_exprt's instance()

src/pointer-analysis/value_set.cpp

@@ -799,8 +799,7 @@ void value_sett::get_value_set_rec(
         static_cast<const typet &>(expr.find("#type"));
 
       dynamic_object_exprt dynamic_object(dynamic_type);
-      dynamic_object.instance()=
-        from_integer(location_number, typet(ID_natural));
+      dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -812,8 +811,7 @@ void value_sett::get_value_set_rec(
       assert(expr_type.id()==ID_pointer);
 
       dynamic_object_exprt dynamic_object(expr_type.subtype());
-      dynamic_object.instance()=
-        from_integer(location_number, typet(ID_natural));
+      dynamic_object.set_instance(location_number);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -897,7 +895,7 @@ void value_sett::get_value_set_rec(
 
     const std::string prefix=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     // first try with suffix
     const std::string full_name=prefix+suffix;
@@ -1392,7 +1390,7 @@ void value_sett::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   for(object_map_dt::const_iterator
       it=object_map.begin();
@@ -1407,7 +1405,7 @@ void value_sett::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1433,10 +1431,10 @@ void value_sett::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1507,7 +1505,7 @@ void value_sett::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &e=get_entry(entryt(name, suffix), lhs.type(), ns);
 

src/pointer-analysis/value_set.h

@@ -115,6 +115,8 @@ class value_sett
 
   typedef std::set<exprt> expr_sett;
 
+  typedef std::set<unsigned int> dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;
   #else

src/pointer-analysis/value_set_fi.cpp

@@ -727,9 +727,8 @@ void value_set_fit::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -742,9 +741,8 @@ void value_set_fit::get_value_set_rec(
       assert(expr.type().id()==ID_pointer);
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert(dest, dynamic_object, 0);
@@ -776,7 +774,7 @@ void value_set_fit::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1322,7 +1320,7 @@ void value_set_fit::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1334,7 +1332,7 @@ void value_set_fit::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1357,10 +1355,10 @@ void value_set_fit::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1452,7 +1450,7 @@ void value_set_fit::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     if(make_union(get_entry(name, suffix).object_map, values_rhs))
       changed = true;

src/pointer-analysis/value_set_fi.h

@@ -155,6 +155,8 @@ class value_set_fit
 
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
+  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;
   typedef std::set<idt> flatten_seent;

src/pointer-analysis/value_set_fivr.cpp

@@ -857,9 +857,8 @@ void value_set_fivrt::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -873,9 +872,8 @@ void value_set_fivrt::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
       // let's make up a unique number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -902,7 +900,7 @@ void value_set_fivrt::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1446,7 +1444,7 @@ void value_set_fivrt::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1458,7 +1456,7 @@ void value_set_fivrt::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1481,10 +1479,10 @@ void value_set_fivrt::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1590,7 +1588,7 @@ void value_set_fivrt::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &temp_entry=get_temporary_entry(name, suffix);
 

src/pointer-analysis/value_set_fivr.h

@@ -216,6 +216,8 @@ class value_set_fivrt
 
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
+  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;
   typedef std::unordered_set<idt, irep_id_hash> flatten_seent;

src/pointer-analysis/value_set_fivrns.cpp

@@ -631,9 +631,8 @@ void value_set_fivrnst::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(dynamic_type);
       // let's make up a `unique' number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -647,9 +646,8 @@ void value_set_fivrnst::get_value_set_rec(
 
       dynamic_object_exprt dynamic_object(expr.type().subtype());
       // let's make up a unique number for this object...
-      dynamic_object.instance()=
-        from_integer(
-          (from_function << 16) | from_target_index, typet(ID_natural));
+      dynamic_object.set_instance(
+        (from_function << 16) | from_target_index);
       dynamic_object.valid()=true_exprt();
 
       insert_from(dest, dynamic_object, 0);
@@ -676,7 +674,7 @@ void value_set_fivrnst::get_value_set_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value)+
+      std::to_string(dynamic_object.get_instance())+
       suffix;
 
     // look it up
@@ -1105,7 +1103,7 @@ void value_set_fivrnst::do_free(
   const object_map_dt &object_map=value_set.read();
 
   // find out which *instances* interest us
-  expr_sett to_mark;
+  dynamic_object_id_sett to_mark;
 
   forall_objects(it, object_map)
   {
@@ -1117,7 +1115,7 @@ void value_set_fivrnst::do_free(
         to_dynamic_object_expr(object);
 
       if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.instance());
+        to_mark.insert(dynamic_object.get_instance());
     }
   }
 
@@ -1140,10 +1138,10 @@ void value_set_fivrnst::do_free(
 
       if(object.id()==ID_dynamic_object)
       {
-        const exprt &instance=
-          to_dynamic_object_expr(object).instance();
+        const dynamic_object_exprt &dynamic_object=
+          to_dynamic_object_expr(object);
 
-        if(to_mark.count(instance)==0)
+        if(to_mark.count(dynamic_object.get_instance())==0)
           set(new_object_map, o_it);
         else
         {
@@ -1225,7 +1223,7 @@ void value_set_fivrnst::assign_rec(
 
     const std::string name=
       "value_set::dynamic_object"+
-      dynamic_object.instance().get_string(ID_value);
+      std::to_string(dynamic_object.get_instance());
 
     entryt &temp_entry = get_temporary_entry(name, suffix);
 

src/pointer-analysis/value_set_fivrns.h

@@ -216,6 +216,8 @@ class value_set_fivrnst
 
   typedef std::unordered_set<exprt, irep_hash> expr_sett;
 
+  typedef std::unordered_set<unsigned int> dynamic_object_id_sett;
+
   #ifdef USE_DSTRING
   typedef std::map<idt, entryt> valuest;
   #else

src/util/std_expr.cpp

@@ -61,6 +61,16 @@ exprt disjunction(const exprt::operandst &op)
   }
 }
 
+void dynamic_object_exprt::set_instance(unsigned int instance)
+{
+  op0()=from_integer(instance, typet(ID_natural));
+}
+
+unsigned int dynamic_object_exprt::get_instance() const
+{
+  return std::stoul(id2string(to_constant_expr(op0()).get_value()));
+}
+
 /*******************************************************************\
 
 Function: conjunction

src/util/std_expr.h

@@ -1505,15 +1505,9 @@ class dynamic_object_exprt:public exprt
     op1().id(ID_unknown);
   }
 
-  exprt &instance()
-  {
-    return op0();
-  }
+  void set_instance(unsigned int instance);
 
-  const exprt &instance() const
-  {
-    return op0();
-  }
+  unsigned int get_instance() const;
 
   exprt &valid()
   {