Skip to content

Commit 63c9a1e

Browse files
author
Joel Allred
authored
Merge pull request #1374 from reuk/reuk/maintain-pointer-invariants
Ensure pointer invariants are maintained
2 parents f77822b + 00e4555 commit 63c9a1e

File tree

18 files changed

+112
-143
lines changed

18 files changed

+112
-143
lines changed

‎CMakeLists.txt

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ cmake_minimum_required(VERSION 3.2)
33
find_program(CCACHE_PROGRAM ccache)
44
if(CCACHE_PROGRAM)
55
set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE "${CCACHE_PROGRAM}")
6+
message(STATUS "Rule launch compile: ${CCACHE_PROGRAM}")
67
endif()
78

89
set(CMAKE_OSX_DEPLOYMENT_TARGET 10.9)
@@ -19,7 +20,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
1920
# Ensure NDEBUG is not set for release builds
2021
set(CMAKE_CXX_FLAGS_RELEASE "-O2")
2122
# Enable lots of warnings
22-
set(CMAKE_CXX_FLAGS "-Wall -Wpedantic -Werror")
23+
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror")
2324
elseif("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
2425
# This would be the place to enable warnings for Windows builds, although
2526
# config.inc doesn't seem to do that currently

‎regression/ansi-c/arch_flags_mcpu_bad/object.intel

91 Bytes
Binary file not shown.

‎regression/ansi-c/arch_flags_mcpu_good/object.arm

34 Bytes
Binary file not shown.

‎regression/ansi-c/arch_flags_mcpu_good/test.desc

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,10 @@ command line:
1414

1515
goto-cc --native-compiler=arm-none-eabi-gcc -mcpu=cortex-a15 -c source.c
1616

17+
On Ubuntu, you can get a suitable compiler using:
18+
19+
sudo apt install gcc-arm-none-eabi
20+
1721
preproc.i is already pre-processed so that it can be linked in without
1822
needing to invoke a pre-processor from a cross-compile toolchain on your
1923
local machine. Linking it together with the ARM object file, while

‎regression/ansi-c/arch_flags_mthumb_bad/object.intel

93 Bytes
Binary file not shown.

‎regression/ansi-c/arch_flags_mthumb_good/object.arm

94 Bytes
Binary file not shown.

‎regression/ansi-c/arch_flags_mthumb_good/test.desc

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,10 @@ line:
1414

1515
goto-cc --native-compiler=arm-none-eabi-gcc -mthumb -c source.c
1616

17+
On Ubuntu, you can get a suitable compiler using:
18+
19+
sudo apt install gcc-arm-none-eabi
20+
1721
preproc.i is already pre-processed so that it can be linked in without
1822
needing to invoke a pre-processor from a cross-compile toolchain on your
1923
local machine. Linking it together with the ARM object file, while

‎src/CMakeLists.txt

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,6 @@ add_subdirectory(util)
165165
add_subdirectory(xmllang)
166166
add_subdirectory(java_bytecode)
167167
add_subdirectory(miniz)
168-
add_subdirectory(musketeer)
169168
add_subdirectory(clobber)
170169
add_subdirectory(cbmc)
171170
add_subdirectory(goto-cc)

‎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/musketeer/CMakeLists.txt

Lines changed: 0 additions & 30 deletions
This file was deleted.

0 commit comments

Comments
 (0)