1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7typedef int Char;
8
9
10Char *tmp;
11
12int glob2 (Char *pathbuf, Char *pathlim)
13{
14 Char *p;
15
16 for (p = pathbuf; p <= pathlim; p++) {
17
18 __VERIFIER_assert(p<=tmp);
19 *p = 1;
20 }
21
22 return 0;
23}
24
25int main ()
26{
27 Char pathbuf[1 +1];
28
29 Char *bound = pathbuf + sizeof(pathbuf)/sizeof(*pathbuf) - 1;
30
31 tmp = pathbuf + sizeof(pathbuf)/sizeof(*pathbuf) - 1;
32
33 glob2 (pathbuf, bound);
34
35 return 0;
36}