Skip to content

Commit 480f19e

Browse files
committed
Check all struct members for possible need for renaming
Don't stop after the first non-pointer element. But really it worked either way, because struct tags are in place everywhere and we don't actually need to rename.
1 parent 1a0b770 commit 480f19e

File tree

3 files changed

+47
-2
lines changed

3 files changed

+47
-2
lines changed

regression/cbmc/vla1/main.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char *argv[])
4+
{
5+
unsigned char x = argc;
6+
// make sure int multiplication below won't overflow - type casting to
7+
// unsigned long long would be possible, but puts yields a challenging problem
8+
// for the SAT solver
9+
__CPROVER_assume(x < 1ULL << (sizeof(int) * 8 / 2 - 1));
10+
11+
struct S
12+
{
13+
int a;
14+
int b[x];
15+
int c;
16+
};
17+
18+
if(x % 2 == 0)
19+
x = 3;
20+
21+
struct S s[x];
22+
23+
__CPROVER_assume(x < 255);
24+
++x;
25+
26+
assert(sizeof(struct S) == ((unsigned char)argc + 2) * sizeof(int));
27+
assert(sizeof(s) == (x - 1) * ((unsigned char)argc + 2) * sizeof(int));
28+
29+
return 0;
30+
}

regression/cbmc/vla1/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/goto_symex_state.cpp

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -618,6 +618,9 @@ void goto_symex_statet::rename_address(
618618
}
619619
}
620620

621+
/// Return true if, and only if, the \p type or one of its subtypes requires SSA
622+
/// renaming. Renaming is necessary when symbol expressions occur within the
623+
/// type, which is the case for arrays of non-constant size.
621624
static bool requires_renaming(const typet &type, const namespacet &ns)
622625
{
623626
if(type.id() == ID_array)
@@ -635,8 +638,12 @@ static bool requires_renaming(const typet &type, const namespacet &ns)
635638
for(auto &component : components)
636639
{
637640
// be careful, or it might get cyclic
638-
if(component.type().id() != ID_pointer)
639-
return requires_renaming(component.type(), ns);
641+
if(
642+
component.type().id() != ID_pointer &&
643+
requires_renaming(component.type(), ns))
644+
{
645+
return true;
646+
}
640647
}
641648

642649
return false;

0 commit comments

Comments
 (0)