[SEC-346] irep_ids: Adding in a NULL-object ID

src/analyses/ai.cpp

@@ -506,7 +506,7 @@ bool ai_baset::do_function_call_rec(
     // We can't really do this here -- we rely on
     // these being removed by some previous analysis.
   }
-  else if(function.id()=="NULL-object")
+  else if(function.id() == ID_null_object)
   {
     // ignore, can't be a function
   }

src/analyses/flow_insensitive_analysis.cpp

@@ -371,7 +371,7 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
       }
     }
   }
-  else if(function.id()=="NULL-object")
+  else if(function.id() == ID_null_object)
   {
     // ignore, can't be a function
   }

src/analyses/goto_rw.cpp

@@ -242,7 +242,7 @@ void rw_range_sett::get_objects_index(
   const range_spect &range_start,
   const range_spect &size)
 {
-  if(expr.array().id()=="NULL-object")
+  if(expr.array().id() == ID_null_object)
     return;
 
   range_spect sub_size=0;
@@ -413,10 +413,10 @@ void rw_range_sett::get_objects_typecast(
 
 void rw_range_sett::get_objects_address_of(const exprt &object)
 {
-  if(object.id()==ID_string_constant ||
-     object.id()==ID_label ||
-     object.id()==ID_array ||
-     object.id()=="NULL-object")
+  if(object.id() == ID_string_constant ||
+     object.id() == ID_label ||
+     object.id() == ID_array ||
+     object.id() == ID_null_object)
     // constant, nothing to do
     return;
   else if(object.id()==ID_symbol)
@@ -558,8 +558,8 @@ void rw_range_sett::get_objects_rec(
     forall_operands(it, expr)
       get_objects_rec(mode, *it);
   }
-  else if(expr.id()=="NULL-object" ||
-          expr.id()==ID_string_constant)
+  else if(expr.id() == ID_null_object ||
+          expr.id() == ID_string_constant)
   {
     // dereferencing may yield some weird ones, ignore these
   }

src/analyses/invariant_set.cpp

@@ -1036,10 +1036,10 @@ void invariant_sett::modifies(const exprt &lhs)
     assert(lhs.operands().size()==2);
     modifies(lhs.op0());
   }
-  else if(lhs.id()=="NULL-object" ||
-          lhs.id()=="is_zero_string" ||
-          lhs.id()=="zero_string" ||
-          lhs.id()=="zero_string_length")
+  else if(lhs.id() == ID_null_object ||
+          lhs.id() == "is_zero_string" ||
+          lhs.id() == "zero_string" ||
+          lhs.id() == "zero_string_length")
   {
     // ignore
   }

src/analyses/static_analysis.cpp

@@ -397,8 +397,8 @@ void static_analysis_baset::do_function_call_rec(
       }
     }
   }
-  else if(function.id()=="NULL-object" ||
-          function.id()==ID_integer_address)
+  else if(function.id() == ID_null_object ||
+          function.id() == ID_integer_address)
   {
     // ignore, can't be a function
   }

src/ansi-c/expr2c.cpp

@@ -3555,10 +3555,7 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()=="pointer_difference")
     return convert_pointer_difference(src, precedence=16);
 
-  else if(src.id()=="NULL-object")
-    return "NULL-object";
-
-  else if(src.id()==ID_null_object)
+  else if(src.id() == ID_null_object)
     return "NULL-object";
 
   else if(src.id()==ID_integer_address ||

src/goto-programs/goto_convert_function_call.cpp

@@ -71,7 +71,7 @@ void goto_convertt::do_function_call(
     do_function_call_symbol(
       new_lhs, to_symbol_expr(new_function), new_arguments, dest);
   }
-  else if(new_function.id()=="NULL-object")
+  else if(new_function.id() == ID_null_object)
   {
   }
   else if(new_function.id()==ID_dereference ||

src/goto-programs/interpreter.cpp

@@ -862,7 +862,7 @@ void interpretert::build_memory_map()
 {
   // put in a dummy for NULL
   memory.resize(1);
-  inverse_memory_map[0]="NULL-OBJECT";
+  inverse_memory_map[0] = ID_null_object;
 
   num_dynamic_objects=0;
   dynamic_types.clear();

src/goto-programs/string_abstraction.cpp

@@ -894,7 +894,7 @@ exprt string_abstractiont::build_unknown(whatt what, bool write)
   typet type=build_type(what);
 
   if(write)
-    return exprt("NULL-object", type);
+    return exprt(ID_null_object, type);
 
   exprt result;
 
@@ -916,7 +916,7 @@ exprt string_abstractiont::build_unknown(whatt what, bool write)
 exprt string_abstractiont::build_unknown(const typet &type, bool write)
 {
   if(write)
-    return exprt("NULL-object", type);
+    return exprt(ID_null_object, type);
 
   // create an uninitialized dummy symbol
   // because of a lack of contextual information we can't build a nice name

src/goto-symex/symex_assign.cpp

@@ -150,11 +150,11 @@ void goto_symext::symex_assign_rec(
   else if(lhs.id()==ID_typecast)
     symex_assign_typecast(
       state, to_typecast_expr(lhs), full_lhs, rhs, guard, assignment_type);
-  else if(lhs.id()==ID_string_constant ||
-          lhs.id()=="NULL-object" ||
-          lhs.id()=="zero_string" ||
-          lhs.id()=="is_zero_string" ||
-          lhs.id()=="zero_string_length")
+  else if(lhs.id() == ID_string_constant ||
+          lhs.id() == ID_null_object ||
+          lhs.id() == "zero_string" ||
+          lhs.id() == "is_zero_string" ||
+          lhs.id() == "zero_string_length")
   {
     // ignore
   }
@@ -355,7 +355,7 @@ void goto_symext::symex_assign_struct_member(
   {
     assert(lhs_struct.operands().size()==1);
 
-    if(lhs_struct.op0().id()=="NULL-object")
+    if(lhs_struct.op0().id() == ID_null_object)
     {
       // ignore, and give up
       return;

src/goto-symex/symex_other.cpp

@@ -34,7 +34,7 @@ void goto_symext::havoc_rec(
       lhs=dest;
     else
       lhs=if_exprt(
-        guard.as_expr(), dest, exprt("NULL-object", dest.type()));
+        guard.as_expr(), dest, exprt(ID_null_object, dest.type()));
 
     code_assignt assignment;
     assignment.lhs()=lhs;

src/pointer-analysis/value_set.cpp

@@ -507,7 +507,7 @@ void value_sett::get_value_set_rec(
     if(expr.get(ID_value)==ID_NULL &&
        expr_type.id()==ID_pointer)
     {
-      insert(dest, exprt("NULL-object", expr_type.subtype()), 0);
+      insert(dest, exprt(ID_null_object, expr_type.subtype()), 0);
     }
     else if(expr_type.id()==ID_unsignedbv ||
             expr_type.id()==ID_signedbv)
@@ -538,7 +538,7 @@ void value_sett::get_value_set_rec(
       // integer-to-pointer
 
       if(expr.op0().is_zero())
-        insert(dest, exprt("NULL-object", expr_type.subtype()), 0);
+        insert(dest, exprt(ID_null_object, expr_type.subtype()), 0);
       else
       {
         // see if we have something for the integer
@@ -1409,7 +1409,7 @@ void value_sett::assign_rec(
     // someone writes into a string-constant
     // evil guy
   }
-  else if(lhs.id()=="NULL-object")
+  else if(lhs.id() == ID_null_object)
   {
     // evil as well
   }

src/pointer-analysis/value_set_dereference.cpp

@@ -301,7 +301,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
   valuet result;
 
-  if(root_object.id()=="NULL-object")
+  if(root_object.id() == ID_null_object)
   {
     if(options.get_bool_option("pointer-check"))
     {

src/pointer-analysis/value_set_fi.cpp

@@ -528,7 +528,7 @@ void value_set_fit::get_value_set_rec(
     if(expr.get(ID_value)==ID_NULL &&
        expr.type().id()==ID_pointer)
     {
-      insert(dest, exprt("NULL-object", expr.type().subtype()), 0);
+      insert(dest, exprt(ID_null_object, expr.type().subtype()), 0);
       return;
     }
   }
@@ -1318,7 +1318,7 @@ void value_set_fit::assign_rec(
     // someone writes into a string-constant
     // evil guy
   }
-  else if(lhs.id()=="NULL-object")
+  else if(lhs.id() == ID_null_object)
   {
     // evil as well
   }

src/pointer-analysis/value_set_fivr.cpp

@@ -645,7 +645,7 @@ void value_set_fivrt::get_value_set_rec(
     if(expr.get(ID_value)==ID_NULL &&
        expr.type().id()==ID_pointer)
     {
-      insert_from(dest, exprt("NULL-object", expr.type().subtype()), 0);
+      insert_from(dest, exprt(ID_null_object, expr.type().subtype()), 0);
       return;
     }
   }
@@ -1456,7 +1456,7 @@ void value_set_fivrt::assign_rec(
     // someone writes into a string-constant
     // evil guy
   }
-  else if(lhs.id()=="NULL-object")
+  else if(lhs.id() == ID_null_object)
   {
     // evil as well
   }

src/pointer-analysis/value_set_fivrns.cpp

@@ -434,7 +434,7 @@ void value_set_fivrnst::get_value_set_rec(
     if(expr.get(ID_value)==ID_NULL &&
        expr.type().id()==ID_pointer)
     {
-      insert_from(dest, exprt("NULL-object", expr.type().subtype()), 0);
+      insert_from(dest, exprt(ID_null_object, expr.type().subtype()), 0);
       return;
     }
   }
@@ -1112,7 +1112,7 @@ void value_set_fivrnst::assign_rec(
     // someone writes into a string-constant
     // evil guy
   }
-  else if(lhs.id()=="NULL-object")
+  else if(lhs.id() == ID_null_object)
   {
     // evil as well
   }

src/solvers/flattening/bv_pointers.cpp

@@ -116,7 +116,7 @@ bool bv_pointerst::convert_address_of_rec(
     add_addr(expr, bv);
     return false;
   }
-  else if(expr.id()=="NULL-object")
+  else if(expr.id() == ID_null_object)
   {
     encode(pointer_logic.get_null_object(), bv);
     return false;

src/util/irep_ids.def

@@ -526,7 +526,7 @@ IREP_ID_ONE(object_size)
 IREP_ID_ONE(good_pointer)
 IREP_ID_ONE(integer_address)
 IREP_ID_ONE(integer_address_object)
-IREP_ID_ONE(null_object)
+IREP_ID_TWO(null_object, NULL-object)
 IREP_ID_ONE(static_object)
 IREP_ID_ONE(stack_object)
 IREP_ID_TWO(C_is_failed_symbol, #is_failed_symbol)

unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -320,7 +320,7 @@ SCENARIO("test_value_set_analysis",
         REQUIRE(exprs_with_id(normal_exprs_after, ID_dynamic_object)==1);
 
         REQUIRE(test_exprs_after.size()==1);
-        REQUIRE(exprs_with_id(test_exprs_after, "NULL-object")==1);
+        REQUIRE(exprs_with_id(test_exprs_after, ID_null_object)==1);
       }
     }
   }