Skip to content

Commit 123162b

Browse files
author
Daniel Kroening
authored
Merge pull request diffblue#1476 from diffblue/remove_ID_reference
Remove ID_reference as front-ends use ID_pointer+ID_C_reference
2 parents 5e1eede + f131b34 commit 123162b

12 files changed

+35
-50
lines changed

‎src/ansi-c/type2name.cpp

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -134,9 +134,12 @@ static std::string type2name(
134134
else if(type.id()==ID_natural)
135135
result+='N';
136136
else if(type.id()==ID_pointer)
137-
result+='*';
138-
else if(type.id()==ID_reference)
139-
result+='&';
137+
{
138+
if(type.get_bool(ID_C_reference))
139+
result+='&';
140+
else
141+
result+='*';
142+
}
140143
else if(type.id()==ID_code)
141144
{
142145
const code_typet &t=to_code_type(type);

‎src/jsil/jsil_typecheck.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,7 @@ void jsil_typecheckt::typecheck_expr_main(exprt &expr)
179179
expr.id()=="builtin_object" ||
180180
expr.id()=="user_object" ||
181181
expr.id()=="object" ||
182-
expr.id()==ID_reference ||
182+
expr.id()==ID_pointer ||
183183
expr.id()==ID_member ||
184184
expr.id()=="variable")
185185
expr.type()=jsil_kind();

‎src/jsil/parser.y

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -614,7 +614,8 @@ jsil_type: TOK_T_NULL
614614
| ref_type
615615
| TOK_T_REFERENCE
616616
{
617-
newstack($$).id(ID_reference);
617+
newstack($$).id(ID_pointer);
618+
newstack($$).set(ID_C_reference, true);
618619
}
619620
;
620621

‎src/solvers/cvc/cvc_conv.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1308,8 +1308,7 @@ void cvc_convt::convert_type(const typet &type)
13081308

13091309
out << " #]";
13101310
}
1311-
else if(type.id()==ID_pointer ||
1312-
type.id()==ID_reference)
1311+
else if(type.id()==ID_pointer)
13131312
{
13141313
out << cvc_pointer_type();
13151314
}

‎src/solvers/flattening/boolbv_width.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -193,8 +193,7 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
193193
{
194194
// no width
195195
}
196-
else if(type_id==ID_pointer ||
197-
type_id==ID_reference)
196+
else if(type_id==ID_pointer)
198197
{
199198
entry.total_width=config.ansi_c.pointer_width;
200199
}

‎src/solvers/flattening/bv_pointers.cpp

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
2626
if(expr.id()==ID_invalid_pointer)
2727
{
2828
if(operands.size()==1 &&
29-
is_ptr(operands[0].type()))
29+
operands[0].type().id()==ID_pointer)
3030
{
3131
const bvt &bv=convert_bv(operands[0]);
3232

@@ -58,7 +58,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
5858
else if(expr.id()==ID_dynamic_object)
5959
{
6060
if(operands.size()==1 &&
61-
is_ptr(operands[0].type()))
61+
operands[0].type().id()==ID_pointer)
6262
{
6363
// we postpone
6464
literalt l=prop.new_variable();
@@ -75,8 +75,8 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
7575
expr.id()==ID_gt || expr.id()==ID_ge)
7676
{
7777
if(operands.size()==2 &&
78-
is_ptr(operands[0].type()) &&
79-
is_ptr(operands[1].type()))
78+
operands[0].type().id()==ID_pointer &&
79+
operands[1].type().id()==ID_pointer)
8080
{
8181
const bvt &bv0=convert_bv(operands[0]);
8282
const bvt &bv1=convert_bv(operands[1]);
@@ -216,7 +216,7 @@ bool bv_pointerst::convert_address_of_rec(
216216

217217
bvt bv_pointerst::convert_pointer_type(const exprt &expr)
218218
{
219-
if(!is_ptr(expr.type()))
219+
if(expr.type().id()!=ID_pointer)
220220
throw "convert_pointer_type got non-pointer type";
221221

222222
// make sure the config hasn't been changed
@@ -444,7 +444,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
444444

445445
bvt bv_pointerst::convert_bitvector(const exprt &expr)
446446
{
447-
if(is_ptr(expr.type()))
447+
if(expr.type().id()==ID_pointer)
448448
return convert_pointer_type(expr);
449449

450450
if(expr.id()==ID_minus &&
@@ -483,7 +483,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
483483
}
484484
else if(expr.id()==ID_pointer_offset &&
485485
expr.operands().size()==1 &&
486-
is_ptr(expr.op0().type()))
486+
expr.op0().type().id()==ID_pointer)
487487
{
488488
bvt op0=convert_bv(expr.op0());
489489

@@ -500,7 +500,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
500500
}
501501
else if(expr.id()==ID_object_size &&
502502
expr.operands().size()==1 &&
503-
is_ptr(expr.op0().type()))
503+
expr.op0().type().id()==ID_pointer)
504504
{
505505
// we postpone until we know the objects
506506
std::size_t width=boolbv_width(expr.type());
@@ -521,7 +521,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
521521
}
522522
else if(expr.id()==ID_pointer_object &&
523523
expr.operands().size()==1 &&
524-
is_ptr(expr.op0().type()))
524+
expr.op0().type().id()==ID_pointer)
525525
{
526526
bvt op0=convert_bv(expr.op0());
527527

@@ -562,7 +562,7 @@ exprt bv_pointerst::bv_get_rec(
562562
std::size_t offset,
563563
const typet &type) const
564564
{
565-
if(!is_ptr(type))
565+
if(type.id()!=ID_pointer)
566566
return SUB::bv_get_rec(bv, unknown, offset, type);
567567

568568
std::string value_addr, value_offset, value;
@@ -605,7 +605,7 @@ exprt bv_pointerst::bv_get_rec(
605605

606606
// we add the elaborated expression as operand
607607
result.copy_to_operands(
608-
pointer_logic.pointer_expr(pointer, type));
608+
pointer_logic.pointer_expr(pointer, to_pointer_type(type)));
609609

610610
return result;
611611
}

‎src/solvers/flattening/bv_pointers.h

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -64,11 +64,6 @@ class bv_pointerst:public boolbvt
6464
postponed_listt postponed_list;
6565

6666
void do_postponed(const postponedt &postponed);
67-
68-
static bool is_ptr(const typet &type)
69-
{
70-
return type.id()==ID_pointer || type.id()==ID_reference;
71-
}
7267
};
7368

7469
#endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H

‎src/solvers/flattening/pointer_logic.cpp

Lines changed: 3 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -65,15 +65,15 @@ std::size_t pointer_logict::add_object(const exprt &expr)
6565

6666
exprt pointer_logict::pointer_expr(
6767
std::size_t object,
68-
const typet &type) const
68+
const pointer_typet &type) const
6969
{
7070
pointert pointer(object, 0);
7171
return pointer_expr(pointer, type);
7272
}
7373

7474
exprt pointer_logict::pointer_expr(
7575
const pointert &pointer,
76-
const typet &type) const
76+
const pointer_typet &type) const
7777
{
7878
if(pointer.object==null_object) // NULL?
7979
{
@@ -109,17 +109,7 @@ exprt pointer_logict::pointer_expr(
109109

110110
exprt deep_object=object_rec(pointer.offset, type, object_expr);
111111

112-
exprt result;
113-
114-
if(type.id()==ID_pointer)
115-
result=exprt(ID_address_of, type);
116-
else if(type.id()==ID_reference)
117-
result=exprt("reference_to", type);
118-
else
119-
assert(0);
120-
121-
result.copy_to_operands(deep_object);
122-
return result;
112+
return address_of_exprt(deep_object, type);
123113
}
124114

125115
exprt pointer_logict::object_rec(

‎src/solvers/flattening/pointer_logic.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/numbering.h>
1818

1919
class namespacet;
20+
class pointer_typet;
2021

2122
class pointer_logict
2223
{
@@ -42,12 +43,12 @@ class pointer_logict
4243
// converts an (object,offset) pair to an expression
4344
exprt pointer_expr(
4445
const pointert &pointer,
45-
const typet &type) const;
46+
const pointer_typet &type) const;
4647

4748
// converts an (object,0) pair to an expression
4849
exprt pointer_expr(
4950
std::size_t object,
50-
const typet &type) const;
51+
const pointer_typet &type) const;
5152

5253
~pointer_logict();
5354
explicit pointer_logict(const namespacet &_ns);

‎src/solvers/smt1/smt1_conv.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,8 @@ exprt smt1_convt::ce_value(
160160
binary2integer(
161161
value.substr(config.bv_encoding.object_bits, std::string::npos), true);
162162

163-
result.copy_to_operands(pointer_logic.pointer_expr(p, type));
163+
result.copy_to_operands(
164+
pointer_logic.pointer_expr(p, to_pointer_type(type)));
164165

165166
return result;
166167
}
@@ -2946,13 +2947,12 @@ void smt1_convt::convert_type(const typet &type)
29462947

29472948
out << "BitVec[" << width << "]";
29482949
}
2949-
else if(type.id()==ID_pointer ||
2950-
type.id()==ID_reference)
2950+
else if(type.id()==ID_pointer)
29512951
{
29522952
std::size_t width=boolbv_width(type);
29532953

29542954
if(width==0)
2955-
throw "failed to get width of pointer/reference";
2955+
throw "failed to get width of pointer";
29562956

29572957
out << "BitVec[" << width << "]";
29582958
}

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -460,7 +460,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
460460
pointer_logict::pointert ptr;
461461
ptr.object=integer2size_t(v/pow);
462462
ptr.offset=v%pow;
463-
return pointer_logic.pointer_expr(ptr, type);
463+
return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
464464
}
465465
else if(type.id()==ID_struct)
466466
{
@@ -4167,8 +4167,7 @@ void smt2_convt::find_symbols(const exprt &expr)
41674167
{
41684168
const exprt &op = expr.op0();
41694169

4170-
if(op.type().id()==ID_pointer ||
4171-
op.type().id()==ID_reference)
4170+
if(op.type().id()==ID_pointer)
41724171
{
41734172
if(object_sizes.find(expr)==object_sizes.end())
41744173
{
@@ -4344,8 +4343,7 @@ void smt2_convt::convert_type(const typet &type)
43444343

43454344
out << "(_ BitVec " << width << ")";
43464345
}
4347-
else if(type.id()==ID_pointer ||
4348-
type.id()==ID_reference)
4346+
else if(type.id()==ID_pointer)
43494347
{
43504348
out << "(_ BitVec "
43514349
<< boolbv_width(type) << ")";

‎src/util/irep_ids.def

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -197,7 +197,6 @@ IREP_ID_ONE(forever)
197197
IREP_ID_ONE(repeat)
198198
IREP_ID_ONE(extractbit)
199199
IREP_ID_ONE(extractbits)
200-
IREP_ID_ONE(reference)
201200
IREP_ID_TWO(C_reference, #reference)
202201
IREP_ID_TWO(C_rvalue_reference, #rvalue_reference)
203202
IREP_ID_ONE(true)

0 commit comments

Comments
 (0)