1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7
8extern void __assert_fail (__const char *__assertion, __const char *__file,
9 unsigned int __line, __const char *__function)
10 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
11extern void __assert_perror_fail (int __errnum, __const char *__file,
12 unsigned int __line,
13 __const char *__function)
14 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
15extern void __assert (const char *__assertion, const char *__file, int __line)
16 __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
17
18typedef struct Toplev {
19 int a;
20 struct Inner {
21 int b;
22 struct Innermost{
23 int c;
24 } *y;
25 } *x;
26} Stuff;
27int main()
28{
29 struct Innermost im = {3};
30 struct Inner inner = {2, &im};
31 struct Toplev good = { 1, &inner};
32 struct Toplev *ptr = &good;
33 ptr->x->y->c = 4;
34 __VERIFIER_assert (ptr->x->y->c == 4);
35 return 0;
36}