Skip to content

Commit a9806c0

Browse files
reukreuk
committed
Ensure pointer invariants are maintained
1 parent a46ad62 commit a9806c0

9 files changed

+27
-33
lines changed

‎src/ansi-c/c_typecast.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -372,8 +372,7 @@ void c_typecastt::implicit_typecast_arithmetic(
372372
case PTR:
373373
if(expr_type.id()==ID_array)
374374
{
375-
new_type.id(ID_pointer);
376-
new_type.subtype()=expr_type.subtype();
375+
new_type=pointer_type(expr_type.subtype());
377376
break;
378377
}
379378
return;

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1594,8 +1594,7 @@ void c_typecheck_baset::typecheck_expr_trinary(if_exprt &expr)
15941594
{
15951595
// Make it void *.
15961596
// gcc and clang issue a warning for this.
1597-
expr.type()=typet(ID_pointer);
1598-
expr.type().subtype()=typet(ID_empty);
1597+
expr.type()=pointer_type(empty_typet());
15991598
implicit_typecast(operands[1], expr.type());
16001599
implicit_typecast(operands[2], expr.type());
16011600
}

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1492,7 +1492,7 @@ void c_typecheck_baset::adjust_function_parameter(typet &type) const
14921492
{
14931493
if(type.id()==ID_array)
14941494
{
1495-
type.id(ID_pointer);
1495+
type=pointer_type(type.subtype());
14961496
type.remove(ID_size);
14971497
type.remove(ID_C_constant);
14981498
}

‎src/ansi-c/parser.y

Lines changed: 7 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -3065,8 +3065,7 @@ unary_identifier_declarator:
30653065
{
30663066
// the type_qualifier_list is for the pointer,
30673067
// and not the identifier_declarator
3068-
stack_type($1).id(ID_pointer);
3069-
stack_type($1).subtype()=typet(ID_abstract);
3068+
stack_type($1)=pointer_type(typet(ID_abstract));
30703069
$2=merge($2, $1); // dest=$2
30713070
make_subtype($3, $2); // dest=$3
30723071
$$=$3;
@@ -3250,15 +3249,13 @@ unary_abstract_declarator:
32503249
'*'
32513250
{
32523251
$$=$1;
3253-
set($$, ID_pointer);
3254-
stack_type($$).subtype()=typet(ID_abstract);
3252+
stack_type($$)=pointer_type(typet(ID_abstract));
32553253
}
32563254
| '*' attribute_type_qualifier_list
32573255
{
32583256
// The type_qualifier_list belongs to the pointer,
32593257
// not to the (missing) abstract declarator.
3260-
set($1, ID_pointer);
3261-
stack_type($1).subtype()=typet(ID_abstract);
3258+
stack_type($1)=pointer_type(typet(ID_abstract));
32623259
$$=merge($2, $1);
32633260
}
32643261
| '*' abstract_declarator
@@ -3270,8 +3267,7 @@ unary_abstract_declarator:
32703267
{
32713268
// The type_qualifier_list belongs to the pointer,
32723269
// not to the abstract declarator.
3273-
stack_type($1).id(ID_pointer);
3274-
stack_type($1).subtype()=typet(ID_abstract);
3270+
stack_type($1)=pointer_type(typet(ID_abstract));
32753271
$2=merge($2, $1); // dest=$2
32763272
make_subtype($3, $2); // dest=$3
32773273
$$=$3;
@@ -3290,15 +3286,13 @@ parameter_unary_abstract_declarator:
32903286
'*'
32913287
{
32923288
$$=$1;
3293-
set($$, ID_pointer);
3294-
stack_type($$).subtype()=typet(ID_abstract);
3289+
stack_type($$)=pointer_type(typet(ID_abstract));
32953290
}
32963291
| '*' attribute_type_qualifier_list
32973292
{
32983293
// The type_qualifier_list belongs to the pointer,
32993294
// not to the (missing) abstract declarator.
3300-
set($1, ID_pointer);
3301-
stack_type($1).subtype()=typet(ID_abstract);
3295+
stack_type($1)=pointer_type(typet(ID_abstract));
33023296
$$=merge($2, $1);
33033297
}
33043298
| '*' parameter_abstract_declarator
@@ -3310,8 +3304,7 @@ parameter_unary_abstract_declarator:
33103304
{
33113305
// The type_qualifier_list belongs to the pointer,
33123306
// not to the (missing) abstract declarator.
3313-
stack($1).id(ID_pointer);
3314-
stack_type($1).subtype()=typet(ID_abstract);
3307+
stack_type($1)=pointer_type(typet(ID_abstract));
33153308
$2=merge($2, $1); // dest=$2
33163309
make_subtype($3, $2); // dest=$3
33173310
$$=$3;

‎src/ansi-c/parser_static.inc

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -290,8 +290,7 @@ Function: make_pointer
290290

291291
static void make_pointer(const YYSTYPE dest)
292292
{
293-
set(dest, ID_pointer);
294-
stack_type(dest).subtype()=typet(ID_abstract);
293+
stack_type(dest)=pointer_type(typet(ID_abstract));
295294
}
296295

297296
/*******************************************************************\

‎src/cpp/cpp_typecheck_constructor.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -41,17 +41,17 @@ static void copy_parent(
4141
exprt &op0=code.op0().op0();
4242

4343
op0.operands().push_back(exprt("cpp-this"));
44-
op0.type().id(ID_pointer);
45-
op0.type().subtype()=cpp_namet(parent_base_name, source_location).as_type();
44+
op0.type()=
45+
pointer_type(cpp_namet(parent_base_name, source_location).as_type());
4646
op0.add_source_location()=source_location;
4747

4848
code.operands().push_back(exprt("explicit-typecast"));
4949
exprt &op1=code.op1();
5050

51-
op1.type().id(ID_pointer);
51+
op0.type()=
52+
pointer_type(cpp_namet(parent_base_name, source_location).as_type());
5253
op1.type().set(ID_C_reference, true);
5354
op1.type().subtype().set(ID_C_constant, true);
54-
op1.type().subtype()=cpp_namet(parent_base_name, source_location).as_type();
5555

5656
op1.operands().push_back(exprt(ID_cpp_name));
5757
op1.op0().get_sub().push_back(irept(ID_name));
@@ -420,9 +420,8 @@ void cpp_typecheckt::default_assignop(
420420
args_decl_declor.name().get_sub().back().add(ID_identifier).id(arg_name);
421421
args_decl_declor.add_source_location()=source_location;
422422

423-
args_decl_declor.type().id(ID_pointer);
423+
args_decl_declor.type()=pointer_type(typet(ID_nil));
424424
args_decl_declor.type().set(ID_C_reference, true);
425-
args_decl_declor.type().subtype().make_nil();
426425
args_decl_declor.value().make_nil();
427426
}
428427

‎src/cpp/parse.cpp

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
1818
#include <util/std_code.h>
1919
#include <util/std_expr.h>
2020
#include <util/std_types.h>
21+
#include <util/c_types.h>
2122

2223
#include <ansi-c/ansi_c_y.tab.h>
2324

@@ -3015,7 +3016,7 @@ bool Parser::optPtrOperator(typet &ptrs)
30153016

30163017
if(t=='*')
30173018
{
3018-
typet op(ID_pointer);
3019+
typet op=pointer_type(typet(ID_nil));
30193020
cpp_tokent tk;
30203021
lex.get_token(tk);
30213022
set_location(op, tk);
@@ -3078,7 +3079,7 @@ bool Parser::optPtrOperator(typet &ptrs)
30783079
{
30793080
cpp_tokent tk;
30803081
lex.get_token(tk);
3081-
typet op(ID_pointer);
3082+
typet op=pointer_type(typet(ID_nil));
30823083
op.set(ID_C_reference, true);
30833084
set_location(op, tk);
30843085
t_list.push_front(op);
@@ -3087,7 +3088,7 @@ bool Parser::optPtrOperator(typet &ptrs)
30873088
{
30883089
cpp_tokent tk;
30893090
lex.get_token(tk);
3090-
typet op(ID_pointer);
3091+
typet op=pointer_type(typet(ID_nil));
30913092
op.set(ID_C_rvalue_reference, true);
30923093
set_location(op, tk);
30933094
t_list.push_front(op);
@@ -3530,7 +3531,7 @@ bool Parser::rPtrToMember(irept &ptr_to_mem)
35303531
std::cout << std::string(__indent, ' ') << "Parser::rPtrToMember 0\n";
35313532
#endif
35323533

3533-
irept ptm(ID_pointer);
3534+
typet ptm=pointer_type(typet(ID_nil));
35343535
irept &name = ptm.add("to-member");
35353536
name=cpp_namet();
35363537
irept::subt &components=name.get_sub();
@@ -6477,7 +6478,7 @@ bool Parser::rPrimaryExpr(exprt &exp)
64776478

64786479
case TOK_NULLPTR:
64796480
lex.get_token(tk);
6480-
exp=constant_exprt(ID_NULL, typet(ID_pointer, typet(ID_nullptr)));
6481+
exp=constant_exprt(ID_NULL, pointer_type(typet(ID_nullptr)));
64816482
set_location(exp, tk);
64826483
#ifdef DEBUG
64836484
std::cout << std::string(__indent, ' ') << "Parser::rPrimaryExpr 6\n";

‎src/goto-programs/remove_exceptions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,7 @@ void remove_exceptionst::add_exceptional_returns(
213213
new_symbol.base_name=id2string(function_symbol.base_name)+EXC_SUFFIX;
214214
new_symbol.name=id2string(function_symbol.name)+EXC_SUFFIX;
215215
new_symbol.mode=function_symbol.mode;
216-
new_symbol.type=typet(ID_pointer, empty_typet());
216+
new_symbol.type=pointer_type(empty_typet());
217217
symbol_table.add(new_symbol);
218218

219219
// initialize the exceptional return with NULL

‎src/util/std_types.h

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1391,6 +1391,7 @@ class pointer_typet:public bitvector_typet
13911391
inline const pointer_typet &to_pointer_type(const typet &type)
13921392
{
13931393
assert(type.id()==ID_pointer);
1394+
assert(!type.get(ID_width).empty());
13941395
return static_cast<const pointer_typet &>(type);
13951396
}
13961397

@@ -1400,6 +1401,7 @@ inline const pointer_typet &to_pointer_type(const typet &type)
14001401
inline pointer_typet &to_pointer_type(typet &type)
14011402
{
14021403
assert(type.id()==ID_pointer);
1404+
assert(!type.get(ID_width).empty());
14031405
return static_cast<pointer_typet &>(type);
14041406
}
14051407

@@ -1428,6 +1430,7 @@ class reference_typet:public pointer_typet
14281430
inline const reference_typet &to_reference_type(const typet &type)
14291431
{
14301432
assert(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1433+
assert(!type.get(ID_width).empty());
14311434
return static_cast<const reference_typet &>(type);
14321435
}
14331436

@@ -1437,6 +1440,7 @@ inline const reference_typet &to_reference_type(const typet &type)
14371440
inline reference_typet &to_reference_type(typet &type)
14381441
{
14391442
assert(type.id()==ID_pointer && type.get_bool(ID_C_reference));
1443+
assert(!type.get(ID_width).empty());
14401444
return static_cast<reference_typet &>(type);
14411445
}
14421446

0 commit comments

Comments
 (0)