Description
CBMC version: 5.11 (cbmc-5.11-103-g1f4da29)
Operating system: 64-bit x86_64 linux
Exact command line resulting in the issue: cbmc <prgname.c>
What behaviour did you expect: no conversion error
What happened instead: Member not found in structure definition conversion error
The bug was introduced by the following commit:
commit 1f4da29
Author: Daniel Kroening [email protected]
Date: Sat Dec 29 18:56:13 2018 +0000
**remove variant of type2name without namespace**
A simple testcase is:
int main()
{
typedef struct onet {
union{struct onet *next;} abc;
} onet;
typedef struct twot {
union{struct twot *next;} xyz;
} twot;
twot two;
two.xyz.next->xyz.next = 0;
return 0;
}
cbmc before the commit will complete and report VERIFICATION SUCCESSFUL.
cbmc after the commit will report:
CBMC version 5.11 (cbmc-5.11-103-g1f4da29) 64-bit x86_64 linux
Parsing sus.c
Converting
Type-checking sus
file sus.c line 12 function main: member xyz' not found in struct onet { union abc; }'
CONVERSION ERROR