Skip to content

Commit b5c07f4

Browse files
committed
symex_allocate: only use alloc_size when set
When alloc_size isn't set but the other conditions in the earlier branch are not satisfied we must not use alloc_size. Fall back to building an array of characters instead.
1 parent f4dedec commit b5c07f4

File tree

3 files changed

+16
-1
lines changed

3 files changed

+16
-1
lines changed

regression/cbmc/Malloc25/main.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#include <stdlib.h>
2+
3+
int main(int argc, char *argv[])
4+
{
5+
int *p = malloc((size_t)argc * (size_t)argc * sizeof(int));
6+
return 0;
7+
}

regression/cbmc/Malloc25/test.desc

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

src/goto-symex/symex_builtin_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ void goto_symext::symex_allocate(
102102

103103
object_type = array_typet(*tmp_type, s);
104104
}
105-
else
105+
else if(alloc_size.has_value())
106106
{
107107
if(*alloc_size == *elem_size)
108108
object_type = *tmp_type;

0 commit comments

Comments
 (0)