Skip to content

Commit d158216

Browse files
authored
Merge pull request #7441 from tautschnig/feature/ptr-diff-mixed-types
C front-end: reject pointer subtraction over distinct types
2 parents 8c18ecd + 206cf2a commit d158216

File tree

6 files changed

+19
-23
lines changed

6 files changed

+19
-23
lines changed

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.c

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

regression/cbmc-incr-smt2/pointer_arithmetic/pointer_subtraction_diff_types.desc

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

regression/cbmc/ptr_arithmetic_on_null/main.c

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,11 @@ void main()
1212
assert(NULL - NULL == 0);
1313

1414
int *ptr;
15+
#ifdef MISSING_CAST
1516
assert(ptr - NULL == 0);
17+
#else
18+
assert(ptr - (int *)NULL == 0);
19+
#endif
1620
ptr = NULL;
1721
assert((ptr - 1) + 1 == NULL);
1822

regression/cbmc/ptr_arithmetic_on_null/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ main.c
55
^\[main.assertion.2\] line .* assertion \(void \*\)0 != \(void \*\)0 - \(.*\)1: SUCCESS$
66
^\[main.assertion.3\] line .* assertion \(void \*\)0 != \(void \*\)0 \+ \(.*\)offset: SUCCESS$
77
^\[main.assertion.4\] line .* assertion \(void \*\)0 - \(void \*\)0 == \(.*\)0: SUCCESS$
8-
^\[main.assertion.5\] line .* assertion ptr - \(void \*\)0 == \(.*\)0: FAILURE$
8+
^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == \(.*\)0: FAILURE$
99
^\[main.assertion.6\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): SUCCESS$
1010
^\[main.assertion.7\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): FAILURE$
1111
^EXIT=10$
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE gcc-only
2+
main.c
3+
-DMISSING_CAST
4+
pointer subtraction over different types
5+
CONVERSION ERROR
6+
^EXIT=6$
7+
^SIGNAL=0$
8+
--
9+
--

src/ansi-c/c_typecheck_expr.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4171,8 +4171,11 @@ void c_typecheck_baset::typecheck_expr_pointer_arithmetic(exprt &expr)
41714171
if(type0.id()==ID_pointer &&
41724172
type1.id()==ID_pointer)
41734173
{
4174-
// We should check the subtypes, and complain if
4175-
// they are really different.
4174+
if(type0 != type1)
4175+
{
4176+
throw invalid_source_file_exceptiont{
4177+
"pointer subtraction over different types", expr.source_location()};
4178+
}
41764179
expr.type()=pointer_diff_type();
41774180
typecheck_arithmetic_pointer(op0);
41784181
typecheck_arithmetic_pointer(op1);

0 commit comments

Comments
 (0)