Skip to content

Commit a743af3

Browse files
authored
Merge pull request #5427 from danpoe/fixes/pointer-validity-check-void-dereference
Fix cbmc crash on pointer checks of void pointer dereferences
2 parents e0e293b + b8f6483 commit a743af3

File tree

5 files changed

+49
-3
lines changed

5 files changed

+49
-3
lines changed

regression/cbmc/void_pointer6/main.c

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
int main()
2+
{
3+
void *p;
4+
*p;
5+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--pointer-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
9+
Checks that cbmc does not crash with --pointer-check on dereference of an
10+
invalid void pointer

regression/cbmc/void_pointer7/main.c

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
int main()
2+
{
3+
int a = 0;
4+
void *p = &a;
5+
*p;
6+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--pointer-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring
9+
--
10+
Checks that cbmc does not crash with --pointer-check on dereference of a valid
11+
void pointer

src/analyses/goto_check.cpp

Lines changed: 17 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1164,10 +1164,24 @@ void goto_checkt::pointer_validity_check(
11641164

11651165
const exprt &pointer=expr.pointer();
11661166

1167-
auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1168-
CHECK_RETURN(size_of_expr_opt.has_value());
1167+
exprt size;
11691168

1170-
auto conditions = address_check(pointer, size_of_expr_opt.value());
1169+
if(expr.type().id() == ID_empty)
1170+
{
1171+
// a dereference *p (with p being a pointer to void) is valid if p points to
1172+
// valid memory (of any size). the smallest possible size of the memory
1173+
// segment p could be pointing to is 1, hence we use this size for the
1174+
// address check
1175+
size = from_integer(1, size_type());
1176+
}
1177+
else
1178+
{
1179+
auto size_of_expr_opt = size_of_expr(expr.type(), ns);
1180+
CHECK_RETURN(size_of_expr_opt.has_value());
1181+
size = size_of_expr_opt.value();
1182+
}
1183+
1184+
auto conditions = address_check(pointer, size);
11711185

11721186
for(const auto &c : conditions)
11731187
{

0 commit comments

Comments
 (0)