1
2
3
4#line 211 "/usr/lib64/gcc/x86_64-suse-linux/4.5/include/stddef.h"
5typedef unsigned long size_t;
6#line 180 "/usr/include/bits/types.h"
7typedef long __ssize_t;
8#line 110 "/usr/include/sys/types.h"
9typedef __ssize_t ssize_t;
10#line 471 "/usr/include/stdlib.h"
11extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
12#line 2 "./assert.h"
13void __blast_assert(void)
14{
15
16 {
17 ERROR:assert(0);
18#line 4
19 goto ERROR;
20}
21}
22#line 87 "/usr/include/fcntl.h"
23extern int open(char const *__file , int __oflag , ...) __attribute__((__nonnull__(1))) ;
24#line 8 "files/fo_test.c"
25extern int __VERIFIER_nondet_int(void);
26int open(char const *__file, int __oflag, ...) {
27 int tmp = __VERIFIER_nondet_int();
28 return tmp;
29}
30int globalState = 0;
31#line 9
32ssize_t l_read(int fd , char *cbuf , size_t count ) ;
33#line 10
34int l_open(char *file , int flags ) ;
35#line 12 "files/fo_test.c"
36int main(int argc , char **argv )
37{ int file ;
38 int tmp ;
39 void *cbuf ;
40 void *tmp___0 ;
41 int a ;
42 ssize_t tmp___1 ;
43 char *__cil_tmp9 ;
44 unsigned int __cil_tmp10 ;
45 size_t __cil_tmp11 ;
46 char *__cil_tmp12 ;
47 size_t __cil_tmp13 ;
48
49 {
50 {
51#line 14
52 __cil_tmp9 = (char *)"unknown";
53#line 14
54 tmp = l_open(__cil_tmp9, 0);
55#line 14
56 file = tmp;
57#line 15
58 __cil_tmp10 = 1U * 100U;
59#line 15
60 __cil_tmp11 = (size_t )__cil_tmp10;
61#line 15
62 tmp___0 = malloc(__cil_tmp11);
63#line 15
64 cbuf = tmp___0;
65#line 16
66 __cil_tmp12 = (char *)cbuf;
67#line 16
68 __cil_tmp13 = (size_t )99;
69#line 16
70 tmp___1 = l_read(file, __cil_tmp12, __cil_tmp13);
71#line 16
72 a = (int )tmp___1;
73 }
74#line 17
75 return (0);
76}
77}
78#line 22
79extern int ( read)() ;
80#line 20 "files/fo_test.c"
81ssize_t l_read(int fd , char *cbuf , size_t count )
82{ int tmp ;
83
84 {
85#line 21
86 if (globalState == 1) {
87
88 } else {
89 {
90#line 21
91 __blast_assert();
92 }
93 }
94 {
95#line 22
96 tmp = read(fd, cbuf, count);
97 }
98#line 22
99 return ((ssize_t )tmp);
100}
101}
102#line 25 "files/fo_test.c"
103int l_open(char *file , int flags )
104{ int fd ;
105 int tmp ;
106 char const *__cil_tmp5 ;
107
108 {
109 {
110#line 26
111 __cil_tmp5 = (char const *)file;
112#line 26
113 tmp = open(__cil_tmp5, flags);
114#line 26
115 fd = tmp;
116 }
117#line 27
118 if (fd > 0) {
119#line 27
120 globalState = 1;
121 } else {
122
123 }
124#line 28
125 return (fd);
126}
127}