Adding in new NULL_object ID to properly represent the string.

Author: JohnDumbell

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;
@@ -416,7 +416,7 @@ 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")
+     object.id()==ID_NULL_object)
     // constant, nothing to do
     return;
   else if(object.id()==ID_symbol)
@@ -558,7 +558,7 @@ void rw_range_sett::get_objects_rec(
     forall_operands(it, expr)
       get_objects_rec(mode, *it);
   }
-  else if(expr.id()=="NULL-object" ||
+  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,7 +1036,7 @@ void invariant_sett::modifies(const exprt &lhs)
     assert(lhs.operands().size()==2);
     modifies(lhs.op0());
   }
-  else if(lhs.id()=="NULL-object" ||
+  else if(lhs.id()==ID_NULL_object ||
           lhs.id()=="is_zero_string" ||
           lhs.id()=="zero_string" ||
           lhs.id()=="zero_string_length")

src/analyses/static_analysis.cpp

@@ -397,7 +397,7 @@ void static_analysis_baset::do_function_call_rec(
       }
     }
   }
-  else if(function.id()=="NULL-object" ||
+  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 || 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/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

@@ -151,7 +151,7 @@ void goto_symext::symex_assign_rec(
     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()==ID_NULL_object ||
           lhs.id()=="zero_string" ||
           lhs.id()=="is_zero_string" ||
           lhs.id()=="zero_string_length")
@@ -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;