Skip to content

Commit 9ff9be8

Browse files
danpoedanpoe
authored
Merge pull request #5346 from danpoe/fixes/address-check
Treat uninitialized pointers like unknown pointers in address_check()
2 parents f891bc1 + 4a3ccb5 commit 9ff9be8

File tree

7 files changed

+61
-30
lines changed

7 files changed

+61
-30
lines changed

‎regression/cbmc/pointer-check-01/test.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
void main()
2+
{
3+
char *p;
4+
5+
if(p == 0)
6+
{
7+
*p;
8+
}
9+
}

‎regression/cbmc/pointer-check-01/test.desc

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
test.c
3+
--pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
Check that pointer check for *p fails when its value is constrained to 0

‎regression/cbmc/pointer-check-02/test.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
void main()
2+
{
3+
char *p;
4+
5+
{
6+
int i;
7+
__CPROVER_assume(p == &i);
8+
}
9+
10+
*p;
11+
}

‎regression/cbmc/pointer-check-02/test.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
test.c
3+
--pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
Check that pointer check for *p fails when its value is constrained to point to
10+
an out-of-scope local variable

‎regression/cbmc/pointer-extra-checks/test.desc

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,13 @@ main.c
88
^\[main.pointer_dereference.3\] .* dereference failure: pointer outside object bounds in \*q: SUCCESS$
99
^\[main.pointer_dereference.4\] .* dereference failure: deallocated dynamic object in \*r: SUCCESS$
1010
^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
11-
^\[main.pointer_dereference.6\] .* dereference failure: pointer uninitialized in \*s: FAILURE$
11+
^\[main.pointer_dereference.6\] .* dereference failure: pointer invalid in \*s: FAILURE$
12+
^\[main.pointer_dereference.7\] .* dereference failure: pointer NULL in \*s: FAILURE$
13+
^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
14+
^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
15+
^\[main.pointer_dereference.10\] .* dereference failure: pointer outside dynamic object bounds in \*s: FAILURE$
16+
^\[main.pointer_dereference.11\] .* dereference failure: pointer outside object bounds in \*s: FAILURE$
17+
^\[main.pointer_dereference.12\] .* dereference failure: invalid integer address in \*s: FAILURE$
1218
^VERIFICATION FAILED$
1319
--
1420
^warning: ignoring
@@ -28,12 +34,6 @@ main.c
2834
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer uninitialized in \*r:
2935
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: dead object in \*r:
3036
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside object bounds in \*r:
31-
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer NULL in \*s:
32-
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer invalid in \*s:
33-
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: deallocated dynamic object in \*s:
34-
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: dead object in \*s:
35-
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside dynamic object bounds in \*s:
36-
^\[main.pointer_dereference.[0-9]+\] .* dereference failure: pointer outside object bounds in \*s:
3737
--
3838
This test ensures that local_bitvector_analysis is correctly labelling obvious
3939
cases of pointers and that --pointer-check is not generating excess assertions.

‎regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ test.c
33
--harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
7-
\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
6+
\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
7+
\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
88
\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
99
\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
1010
\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS

‎src/analyses/goto_check.cpp

Lines changed: 13 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1282,30 +1282,24 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
12821282
const exprt in_bounds_of_some_explicit_allocation =
12831283
disjunction(alloc_disjuncts);
12841284

1285-
if(flags.is_unknown() || flags.is_null())
1286-
{
1287-
conditions.push_back(conditiont(
1288-
or_exprt(
1289-
in_bounds_of_some_explicit_allocation,
1290-
not_exprt(null_pointer(address))),
1291-
"pointer NULL"));
1292-
}
1285+
const bool unknown = flags.is_unknown() || flags.is_uninitialized();
12931286

1294-
if(flags.is_unknown())
1287+
if(unknown)
12951288
{
12961289
conditions.push_back(conditiont{
12971290
not_exprt{is_invalid_pointer_exprt{address}}, "pointer invalid"});
12981291
}
12991292

1300-
if(flags.is_uninitialized())
1293+
if(unknown || flags.is_null())
13011294
{
1302-
conditions.push_back(
1303-
conditiont{or_exprt{in_bounds_of_some_explicit_allocation,
1304-
not_exprt{is_invalid_pointer_exprt{address}}},
1305-
"pointer uninitialized"});
1295+
conditions.push_back(conditiont(
1296+
or_exprt(
1297+
in_bounds_of_some_explicit_allocation,
1298+
not_exprt(null_pointer(address))),
1299+
"pointer NULL"));
13061300
}
13071301

1308-
if(flags.is_unknown() || flags.is_dynamic_heap())
1302+
if(unknown || flags.is_dynamic_heap())
13091303
{
13101304
conditions.push_back(conditiont(
13111305
or_exprt(
@@ -1314,7 +1308,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
13141308
"deallocated dynamic object"));
13151309
}
13161310

1317-
if(flags.is_unknown() || flags.is_dynamic_local())
1311+
if(unknown || flags.is_dynamic_local())
13181312
{
13191313
conditions.push_back(conditiont(
13201314
or_exprt(
@@ -1323,7 +1317,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
13231317
"dead object"));
13241318
}
13251319

1326-
if(flags.is_unknown() || flags.is_dynamic_heap())
1320+
if(unknown || flags.is_dynamic_heap())
13271321
{
13281322
const or_exprt object_bounds_violation(
13291323
object_lower_bound(address, nil_exprt()),
@@ -1337,9 +1331,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
13371331
"pointer outside dynamic object bounds"));
13381332
}
13391333

1340-
if(
1341-
flags.is_unknown() || flags.is_dynamic_local() ||
1342-
flags.is_static_lifetime())
1334+
if(unknown || flags.is_dynamic_local() || flags.is_static_lifetime())
13431335
{
13441336
const or_exprt object_bounds_violation(
13451337
object_lower_bound(address, nil_exprt()),
@@ -1354,7 +1346,7 @@ goto_checkt::address_check(const exprt &address, const exprt &size)
13541346
"pointer outside object bounds"));
13551347
}
13561348

1357-
if(flags.is_unknown() || flags.is_integer_address())
1349+
if(unknown || flags.is_integer_address())
13581350
{
13591351
conditions.push_back(conditiont(
13601352
implies_exprt(

0 commit comments

Comments
 (0)