Skip to content

Commit e3ad659

Browse files
author
Daniel Kroening
authored
Merge pull request #955 from tautschnig/void-cast
Properly handle void*
2 parents 5e6b593 + 7f6443b commit e3ad659

File tree

95 files changed

+250
-135
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

95 files changed

+250
-135
lines changed

‎regression/cbmc/void_pointer1/main.c

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
char buffer[2];
2+
int length = 2;
3+
4+
void func(void* buf, int len)
5+
{
6+
while( len-- )
7+
*(char *)buf++;
8+
}
9+
10+
void main(){
11+
func(buffer,length);
12+
}

‎regression/cbmc/void_pointer1/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/cbmc/void_pointer2/main.c

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
char buffer[2];
2+
int length = 2;
3+
4+
void func(void* buf, int len)
5+
{
6+
while( len-- )
7+
*(char *)buf++;
8+
}
9+
10+
void main(){
11+
func(buffer,length);
12+
}

‎regression/cbmc/void_pointer2/test.desc

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--pointer-check --no-simplify --unwind 3
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎src/analyses/goto_check.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -1238,7 +1238,8 @@ void goto_checkt::bounds_check(
12381238
plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
12391239

12401240
assert(effective_offset.op0().type()==effective_offset.op1().type());
1241-
assert(effective_offset.type()==size.type());
1241+
if(effective_offset.type()!=size.type())
1242+
size.make_typecast(effective_offset.type());
12421243

12431244
binary_relation_exprt inequality(effective_offset, ID_lt, size);
12441245

‎src/analyses/goto_rw.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -149,6 +149,7 @@ void rw_range_sett::get_objects_complex(
149149

150150
range_spect sub_size=
151151
to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
152+
assert(sub_size>0);
152153
range_spect offset=
153154
(range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
154155

‎src/analyses/invariant_set.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/base_type.h>
1717
#include <util/std_types.h>
1818

19-
#include <ansi-c/c_types.h>
19+
#include <util/c_types.h>
2020
#include <langapi/language_util.h>
2121

2222
#include "invariant_set.h"

‎src/analyses/local_bitvector_analysis.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include <util/std_code.h>
1414
#include <util/expr_util.h>
1515

16-
#include <ansi-c/c_types.h>
16+
#include <util/c_types.h>
1717
#include <langapi/language_util.h>
1818

1919
#include "local_bitvector_analysis.h"

‎src/analyses/local_cfg.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <util/std_code.h>
1515
#include <util/expr_util.h>
1616

17-
#include <ansi-c/c_types.h>
17+
#include <util/c_types.h>
1818
#include <langapi/language_util.h>
1919

2020
#endif

‎src/analyses/local_may_alias.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include <util/std_expr.h>
1414
#include <util/std_code.h>
1515

16-
#include <ansi-c/c_types.h>
16+
#include <util/c_types.h>
1717
#include <langapi/language_util.h>
1818

1919
#include "local_may_alias.h"

‎src/ansi-c/Makefile

-1
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@ SRC = anonymous_member.cpp \
2424
c_typecheck_initializer.cpp \
2525
c_typecheck_type.cpp \
2626
c_typecheck_typecast.cpp \
27-
c_types.cpp \
2827
cprover_library.cpp \
2928
designator.cpp \
3029
expr2c.cpp \

‎src/ansi-c/ansi_c_convert_type.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
88

99
#include <cassert>
1010

11+
#include <util/c_types.h>
1112
#include <util/namespace.h>
1213
#include <util/simplify_expr.h>
1314
#include <util/config.h>

‎src/ansi-c/ansi_c_convert_type.h

-1
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include <util/message.h>
1313

14-
#include "c_types.h"
1514
#include "c_qualifiers.h"
1615
#include "c_storage_spec.h"
1716

‎src/ansi-c/ansi_c_entry_point.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
1717
#include <util/cprover_prefix.h>
1818
#include <util/prefix.h>
1919

20-
#include <ansi-c/c_types.h>
20+
#include <util/c_types.h>
2121
#include <ansi-c/string_constant.h>
2222

2323
#include <goto-programs/goto_functions.h>

‎src/ansi-c/c_nondet_symbol_factory.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: DiffBlue Limited. All rights reserved.
1010
#include <sstream>
1111

1212
#include <util/arith_tools.h>
13+
#include <util/c_types.h>
1314
#include <util/fresh_symbol.h>
1415
#include <util/std_types.h>
1516
#include <util/std_code.h>
@@ -20,7 +21,6 @@ Author: DiffBlue Limited. All rights reserved.
2021

2122
#include <linking/zero_initializer.h>
2223

23-
#include <ansi-c/c_types.h>
2424
#include <ansi-c/string_constant.h>
2525

2626
#include <goto-programs/goto_functions.h>

‎src/ansi-c/c_preprocess.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121

2222
#include <fstream>
2323

24+
#include <util/c_types.h>
2425
#include <util/config.h>
2526
#include <util/message.h>
2627
#include <util/tempfile.h>
@@ -29,7 +30,6 @@ Author: Daniel Kroening, [email protected]
2930
#include <util/std_types.h>
3031
#include <util/prefix.h>
3132

32-
#include "c_types.h"
3333
#include "c_preprocess.h"
3434

3535
#define GCC_DEFINES_16 \

‎src/ansi-c/c_sizeof.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9+
#include <util/c_types.h>
910
#include <util/config.h>
1011
#include <util/arith_tools.h>
1112
#include <util/simplify_expr.h>
1213
#include <util/std_expr.h>
1314

1415
#include "c_sizeof.h"
1516
#include "c_typecast.h"
16-
#include "c_types.h"
1717

1818
/*******************************************************************\
1919

‎src/ansi-c/c_typecast.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include <cassert>
1212

1313
#include <util/arith_tools.h>
14+
#include <util/c_types.h>
1415
#include <util/config.h>
1516
#include <util/expr_util.h>
1617
#include <util/std_expr.h>
@@ -19,7 +20,6 @@ Author: Daniel Kroening, [email protected]
1920
#include <util/simplify_expr.h>
2021

2122
#include "c_typecast.h"
22-
#include "c_types.h"
2323
#include "c_qualifiers.h"
2424

2525
/*******************************************************************\

‎src/ansi-c/c_typecheck_expr.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include <cassert>
1010

1111
#include <util/arith_tools.h>
12+
#include <util/c_types.h>
1213
#include <util/config.h>
1314
#include <util/std_types.h>
1415
#include <util/prefix.h>
@@ -19,7 +20,6 @@ Author: Daniel Kroening, [email protected]
1920
#include <util/pointer_offset_size.h>
2021
#include <util/pointer_predicates.h>
2122

22-
#include "c_types.h"
2323
#include "c_typecast.h"
2424
#include "c_typecheck_base.h"
2525
#include "c_sizeof.h"
@@ -1318,8 +1318,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
13181318
// an integer/float of the same size
13191319
if((expr_type.id()==ID_signedbv ||
13201320
expr_type.id()==ID_unsignedbv) &&
1321-
pointer_offset_size(expr_type, *this)==
1322-
pointer_offset_size(op_vector_type, *this))
1321+
pointer_offset_bits(expr_type, *this)==
1322+
pointer_offset_bits(op_vector_type, *this))
13231323
{
13241324
}
13251325
else

‎src/ansi-c/c_typecheck_initializer.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99
#include <util/arith_tools.h>
10+
#include <util/c_types.h>
1011
#include <util/config.h>
1112
#include <util/type_eq.h>
1213
#include <util/std_types.h>
@@ -16,7 +17,6 @@ Author: Daniel Kroening, [email protected]
1617

1718
#include <linking/zero_initializer.h>
1819

19-
#include "c_types.h"
2020
#include "c_typecheck_base.h"
2121
#include "string_constant.h"
2222
#include "anonymous_member.h"

‎src/ansi-c/c_typecheck_type.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -8,14 +8,14 @@ Author: Daniel Kroening, [email protected]
88

99
#include <unordered_set>
1010

11+
#include <util/c_types.h>
1112
#include <util/config.h>
1213
#include <util/simplify_expr.h>
1314
#include <util/arith_tools.h>
1415
#include <util/std_types.h>
1516
#include <util/pointer_offset_size.h>
1617

1718
#include "c_typecheck_base.h"
18-
#include "c_types.h"
1919
#include "c_sizeof.h"
2020
#include "c_qualifiers.h"
2121
#include "ansi_c_declaration.h"

‎src/ansi-c/c_typecheck_typecast.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ Author: Daniel Kroening, [email protected]
88

99
#include "c_typecast.h"
1010
#include "c_typecheck_base.h"
11-
#include "c_types.h"
1211

1312
/*******************************************************************\
1413

‎src/ansi-c/expr2c.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
2020
#include <set>
2121

2222
#include <util/arith_tools.h>
23+
#include <util/c_types.h>
2324
#include <util/config.h>
2425
#include <util/std_types.h>
2526
#include <util/std_code.h>
@@ -37,7 +38,6 @@ Author: Daniel Kroening, [email protected]
3738
#include "c_misc.h"
3839
#include "c_qualifiers.h"
3940
#include "expr2c.h"
40-
#include "c_types.h"
4141
#include "expr2c_class.h"
4242

4343
/*

‎src/ansi-c/literals/convert_character_literal.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,9 @@ Author: Daniel Kroening, [email protected]
99
#include <cassert>
1010

1111
#include <util/arith_tools.h>
12+
#include <util/c_types.h>
1213
#include <util/std_expr.h>
1314

14-
#include "../c_types.h"
15-
1615
#include "unescape_string.h"
1716
#include "convert_character_literal.h"
1817

‎src/ansi-c/literals/convert_float_literal.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,13 @@ Author: Daniel Kroening, [email protected]
99
#include <cassert>
1010

1111
#include <util/arith_tools.h>
12+
#include <util/c_types.h>
1213
#include <util/config.h>
1314
#include <util/ieee_float.h>
1415
#include <util/std_expr.h>
1516
#include <util/std_types.h>
1617
#include <util/string2int.h>
1718

18-
#include "../c_types.h"
1919
#include "parse_float.h"
2020
#include "convert_float_literal.h"
2121

‎src/ansi-c/literals/convert_string_literal.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,10 @@ Author: Daniel Kroening, [email protected]
99
#include <cassert>
1010

1111
#include <util/arith_tools.h>
12+
#include <util/c_types.h>
1213
#include <util/unicode.h>
1314

1415
#include "../string_constant.h"
15-
#include "../c_types.h"
1616

1717
#include "unescape_string.h"
1818
#include "convert_string_literal.h"

‎src/ansi-c/padding.cpp

+3
Original file line numberDiff line numberDiff line change
@@ -339,6 +339,9 @@ void add_padding(union_typet &type, const namespacet &ns)
339339
mp_integer max_alignment=alignment(type, ns)*8;
340340
mp_integer size_bits=pointer_offset_bits(type, ns);
341341

342+
if(size_bits<0)
343+
throw "type of unknown size:\n"+type.pretty();
344+
342345
union_typet::componentst &components=type.components();
343346

344347
// Is the union packed?

‎src/ansi-c/parser_static.inc

+1-2
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,9 @@
1+
#include <util/c_types.h>
12
#include <util/std_code.h>
23
#include <util/std_types.h>
34
#include <util/std_expr.h>
45
#include <util/string2int.h>
56

6-
#include "c_types.h"
7-
87
#define YYSTYPE unsigned
98
#define YYSTYPE_IS_TRIVIAL 1
109

‎src/ansi-c/printf_formatter.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,10 @@ Author: Daniel Kroening, [email protected]
99
#include <cassert>
1010
#include <sstream>
1111

12+
#include <util/c_types.h>
1213
#include <util/format_constant.h>
1314
#include <util/simplify_expr.h>
1415

15-
#include "c_types.h"
1616
#include "printf_formatter.h"
1717

1818
/*******************************************************************\

‎src/ansi-c/scanner.l

-1
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ static int isatty(int) { return 0; }
2121

2222
#include <util/unicode.h>
2323

24-
#include "c_types.h"
2524
#include "preprocessor_line.h"
2625
#include "string_constant.h"
2726

‎src/ansi-c/string_constant.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,10 @@ Author: Daniel Kroening, [email protected]
77
\*******************************************************************/
88

99
#include <util/arith_tools.h>
10+
#include <util/c_types.h>
1011
#include <util/std_expr.h>
1112

1213
#include "string_constant.h"
13-
#include "c_types.h"
1414

1515
/*******************************************************************\
1616

‎src/cpp/cpp_constructor.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include <util/arith_tools.h>
1010
#include <util/std_types.h>
1111

12-
#include <ansi-c/c_types.h>
12+
#include <util/c_types.h>
1313

1414
#include "cpp_typecheck.h"
1515
#include "cpp_util.h"

‎src/cpp/cpp_convert_type.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include <util/arith_tools.h>
1313
#include <util/std_types.h>
1414

15-
#include <ansi-c/c_types.h>
15+
#include <util/c_types.h>
1616

1717
#include "cpp_convert_type.h"
1818
#include "cpp_declaration.h"

‎src/cpp/cpp_declarator_converter.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include <util/source_location.h>
1010
#include <util/std_types.h>
1111

12-
#include <ansi-c/c_types.h>
12+
#include <util/c_types.h>
1313

1414
#include "cpp_type2name.h"
1515
#include "cpp_declarator_converter.h"

0 commit comments

Comments
 (0)