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;

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

@@ -527,6 +527,7 @@ 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)