Remove ID_reference as front-ends use ID_pointer+ID_C_reference

Author: tautschnig

src/ansi-c/type2name.cpp

@@ -134,9 +134,12 @@ static std::string type2name(
   else if(type.id()==ID_natural)
     result+='N';
   else if(type.id()==ID_pointer)
-    result+='*';
-  else if(type.id()==ID_reference)
-    result+='&';
+  {
+    if(type.get_bool(ID_C_reference))
+      result+='&';
+    else
+      result+='*';
+  }
   else if(type.id()==ID_code)
   {
     const code_typet &t=to_code_type(type);

src/jsil/jsil_typecheck.cpp

@@ -178,7 +178,7 @@ void jsil_typecheckt::typecheck_expr_main(exprt &expr)
             expr.id()=="builtin_object" ||
             expr.id()=="user_object" ||
             expr.id()=="object" ||
-            expr.id()==ID_reference ||
+            expr.id()==ID_pointer ||
             expr.id()==ID_member ||
             expr.id()=="variable")
       expr.type()=jsil_kind();

src/jsil/parser.y

@@ -614,7 +614,8 @@ jsil_type: TOK_T_NULL
          | ref_type
          | TOK_T_REFERENCE
          {
-           newstack($$).id(ID_reference);
+           newstack($$).id(ID_pointer);
+           newstack($$).set(ID_C_reference, true);
          }
          ;
 

src/solvers/cvc/cvc_conv.cpp

@@ -1308,8 +1308,7 @@ void cvc_convt::convert_type(const typet &type)
 
     out << " #]";
   }
-  else if(type.id()==ID_pointer ||
-          type.id()==ID_reference)
+  else if(type.id()==ID_pointer)
   {
     out << cvc_pointer_type();
   }

src/solvers/dplib/dplib_conv.cpp

@@ -1116,8 +1116,7 @@ void dplib_convt::convert_dplib_type(const typet &type)
 
     dplib_prop.out << " #]";
   }
-  else if(type.id()==ID_pointer ||
-          type.id()==ID_reference)
+  else if(type.id()==ID_pointer)
   {
     dplib_prop.out << dplib_pointer_type();
   }

src/solvers/flattening/bv_pointers.cpp

@@ -26,7 +26,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
   if(expr.id()==ID_invalid_pointer)
   {
     if(operands.size()==1 &&
-       is_ptr(operands[0].type()))
+       operands[0].type().id()==ID_pointer)
     {
       const bvt &bv=convert_bv(operands[0]);
 
@@ -58,7 +58,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
   else if(expr.id()==ID_dynamic_object)
   {
     if(operands.size()==1 &&
-       is_ptr(operands[0].type()))
+       operands[0].type().id()==ID_pointer)
     {
       // we postpone
       literalt l=prop.new_variable();
@@ -75,8 +75,8 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
           expr.id()==ID_gt || expr.id()==ID_ge)
   {
     if(operands.size()==2 &&
-       is_ptr(operands[0].type()) &&
-       is_ptr(operands[1].type()))
+       operands[0].type().id()==ID_pointer &&
+       operands[1].type().id()==ID_pointer)
     {
       const bvt &bv0=convert_bv(operands[0]);
       const bvt &bv1=convert_bv(operands[1]);
@@ -217,7 +217,7 @@ bool bv_pointerst::convert_address_of_rec(
 
 bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 {
-  if(!is_ptr(expr.type()))
+  if(expr.type().id()!=ID_pointer)
     throw "convert_pointer_type got non-pointer type";
 
   // make sure the config hasn't been changed
@@ -445,7 +445,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
 bvt bv_pointerst::convert_bitvector(const exprt &expr)
 {
-  if(is_ptr(expr.type()))
+  if(expr.type().id()==ID_pointer)
     return convert_pointer_type(expr);
 
   if(expr.id()==ID_minus &&
@@ -484,7 +484,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_pointer_offset &&
           expr.operands().size()==1 &&
-          is_ptr(expr.op0().type()))
+          expr.op0().type().id()==ID_pointer)
   {
     bvt op0=convert_bv(expr.op0());
 
@@ -501,7 +501,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_object_size &&
           expr.operands().size()==1 &&
-          is_ptr(expr.op0().type()))
+          expr.op0().type().id()==ID_pointer)
   {
     // we postpone until we know the objects
     std::size_t width=boolbv_width(expr.type());
@@ -522,7 +522,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
   }
   else if(expr.id()==ID_pointer_object &&
           expr.operands().size()==1 &&
-          is_ptr(expr.op0().type()))
+          expr.op0().type().id()==ID_pointer)
   {
     bvt op0=convert_bv(expr.op0());
 
@@ -563,7 +563,7 @@ exprt bv_pointerst::bv_get_rec(
   std::size_t offset,
   const typet &type) const
 {
-  if(!is_ptr(type))
+  if(type.id()!=ID_pointer)
     return SUB::bv_get_rec(bv, unknown, offset, type);
 
   std::string value_addr, value_offset, value;

src/solvers/flattening/bv_pointers.h

@@ -64,11 +64,6 @@ class bv_pointerst:public boolbvt
   postponed_listt postponed_list;
 
   void do_postponed(const postponedt &postponed);
-
-  static bool is_ptr(const typet &type)
-  {
-    return type.id()==ID_pointer || type.id()==ID_reference;
-  }
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H

src/solvers/flattening/pointer_logic.cpp

@@ -112,9 +112,12 @@ exprt pointer_logict::pointer_expr(
   exprt result;
 
   if(type.id()==ID_pointer)
-    result=exprt(ID_address_of, type);
-  else if(type.id()==ID_reference)
-    result=exprt("reference_to", type);
+  {
+    if(type.get_bool(ID_C_reference))
+      result=exprt("reference_to", type);
+    else
+      result=exprt(ID_address_of, type);
+  }
   else
     assert(0);
 

src/solvers/smt1/smt1_conv.cpp

@@ -2946,13 +2946,12 @@ void smt1_convt::convert_type(const typet &type)
 
     out << "BitVec[" << width << "]";
   }
-  else if(type.id()==ID_pointer ||
-          type.id()==ID_reference)
+  else if(type.id()==ID_pointer)
   {
     std::size_t width=boolbv_width(type);
 
     if(width==0)
-      throw "failed to get width of pointer/reference";
+      throw "failed to get width of pointer";
 
     out << "BitVec[" << width << "]";
   }

src/solvers/smt2/smt2_conv.cpp

@@ -4167,8 +4167,7 @@ void smt2_convt::find_symbols(const exprt &expr)
   {
     const exprt &op = expr.op0();
 
-    if(op.type().id()==ID_pointer ||
-       op.type().id()==ID_reference)
+    if(op.type().id()==ID_pointer)
     {
       if(object_sizes.find(expr)==object_sizes.end())
       {
@@ -4344,8 +4343,7 @@ void smt2_convt::convert_type(const typet &type)
 
     out << "(_ BitVec " << width << ")";
   }
-  else if(type.id()==ID_pointer ||
-          type.id()==ID_reference)
+  else if(type.id()==ID_pointer)
   {
     out << "(_ BitVec "
         << boolbv_width(type) << ")";