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/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;
@@ -606,7 +606,7 @@ exprt bv_pointerst::bv_get_rec(
 
   // we add the elaborated expression as operand
   result.copy_to_operands(
-    pointer_logic.pointer_expr(pointer, type));
+    pointer_logic.pointer_expr(pointer, to_pointer_type(type)));
 
   return result;
 }

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

@@ -65,15 +65,15 @@ std::size_t pointer_logict::add_object(const exprt &expr)
 
 exprt pointer_logict::pointer_expr(
   std::size_t object,
-  const typet &type) const
+  const pointer_typet &type) const
 {
   pointert pointer(object, 0);
   return pointer_expr(pointer, type);
 }
 
 exprt pointer_logict::pointer_expr(
   const pointert &pointer,
-  const typet &type) const
+  const pointer_typet &type) const
 {
   if(pointer.object==null_object) // NULL?
   {
@@ -109,17 +109,7 @@ exprt pointer_logict::pointer_expr(
 
   exprt deep_object=object_rec(pointer.offset, type, object_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);
-  else
-    assert(0);
-
-  result.copy_to_operands(deep_object);
-  return result;
+  return address_of_exprt(deep_object, type);
 }
 
 exprt pointer_logict::object_rec(

src/solvers/flattening/pointer_logic.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/numbering.h>
 
 class namespacet;
+class pointer_typet;
 
 class pointer_logict
 {
@@ -42,12 +43,12 @@ class pointer_logict
   // converts an (object,offset) pair to an expression
   exprt pointer_expr(
     const pointert &pointer,
-    const typet &type) const;
+    const pointer_typet &type) const;
 
   // converts an (object,0) pair to an expression
   exprt pointer_expr(
     std::size_t object,
-    const typet &type) const;
+    const pointer_typet &type) const;
 
   ~pointer_logict();
   explicit pointer_logict(const namespacet &_ns);

src/solvers/smt1/smt1_conv.cpp

@@ -160,7 +160,8 @@ exprt smt1_convt::ce_value(
       binary2integer(
         value.substr(config.bv_encoding.object_bits, std::string::npos), true);
 
-    result.copy_to_operands(pointer_logic.pointer_expr(p, type));
+    result.copy_to_operands(
+      pointer_logic.pointer_expr(p, to_pointer_type(type)));
 
     return result;
   }
@@ -2946,13 +2947,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

@@ -460,7 +460,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
     pointer_logict::pointert ptr;
     ptr.object=integer2size_t(v/pow);
     ptr.offset=v%pow;
-    return pointer_logic.pointer_expr(ptr, type);
+    return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
   }
   else if(type.id()==ID_struct)
   {
@@ -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) << ")";