Merge pull request diffblue#2048 from JohnDumbell/improvement/adding_null_object_id

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

Author: Daniel Kroening

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

@@ -3556,10 +3556,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;