Showing error 221

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: list-properties/list_flag.cil.c
Line in file: 204
Project: SV-COMP 2012
Tools: Manual Work
Entered: 2012-11-19 13:47:39 UTC

Source: 

  1/* Generated by CIL v. 1.3.7 */
  2/* print_CIL_Input is true */
  3
  4#line 211 "/usr/lib/x86_64-linux-gnu/gcc/x86_64-linux-gnu/4.5.2/include/stddef.h"
  5typedef unsigned long size_t;
  6#line 471 "/usr/include/stdlib.h"
  7extern  __attribute__((__nothrow__)) void *malloc(size_t __size )  __attribute__((__malloc__)) ;
  8
  9#line 14 "list_flag.c"
 10struct node {
 11   int h ;
 12   struct node *n ;
 13};
 14#line 14 "list_flag.c"
 15typedef struct node *List;
 16#line 10 "list_flag.c"
 17void exit(int s ) 
 18{ 
 19
 20  {
 21  _EXIT: 
 22  goto _EXIT;
 23}
 24}
 25#line 20
 26extern int ( /* missing proto */  __VERIFIER_nondet_int)() ;
 27#line 19 "list_flag.c"
 28void main(void) 
 29{ int flag ;
 30  int tmp ;
 31  List p ;
 32  List a ;
 33  List t ;
 34  void* tmp___0 ;
 35  void* tmp___1 ;
 36  int tmp___2 ;
 37  List __cil_tmp9 ;
 38  unsigned int __cil_tmp10 ;
 39  unsigned int __cil_tmp11 ;
 40  List __cil_tmp12 ;
 41  unsigned int __cil_tmp13 ;
 42  unsigned int __cil_tmp14 ;
 43  unsigned int __cil_tmp15 ;
 44  unsigned int __cil_tmp16 ;
 45  unsigned int __cil_tmp17 ;
 46  unsigned int __cil_tmp18 ;
 47  int __cil_tmp19 ;
 48  unsigned int __cil_tmp20 ;
 49  unsigned int __cil_tmp21 ;
 50  int __cil_tmp22 ;
 51  unsigned int __cil_tmp23 ;
 52  unsigned int __cil_tmp24 ;
 53  int __cil_tmp25 ;
 54
 55  {
 56  {
 57#line 20
 58  tmp = __VERIFIER_nondet_int();
 59#line 20
 60  flag = tmp;
 61#line 26
 62  tmp___0 = malloc(8U);
 63#line 26
 64  a = (struct node *)tmp___0;
 65  }
 66  {
 67#line 27
 68  __cil_tmp9 = (List )0;
 69#line 27
 70  __cil_tmp10 = (unsigned int )__cil_tmp9;
 71#line 27
 72  __cil_tmp11 = (unsigned int )a;
 73#line 27
 74  if (__cil_tmp11 == __cil_tmp10) {
 75    {
 76#line 27
 77    exit(1);
 78    }
 79  } else {
 80
 81  }
 82  }
 83#line 28
 84  p = a;
 85  {
 86#line 29
 87  while (1) {
 88    while_0_continue: /* CIL Label */ ;
 89    {
 90#line 29
 91    tmp___2 = __VERIFIER_nondet_int();
 92    }
 93#line 29
 94    if (tmp___2) {
 95
 96    } else {
 97      goto while_0_break;
 98    }
 99#line 30
100    if (flag) {
101#line 31
102      *((int *)p) = 1;
103    } else {
104#line 33
105      *((int *)p) = 2;
106    }
107    {
108#line 37
109    tmp___1 = malloc(8U);
110#line 37
111    t = (struct node *)tmp___1;
112    }
113    {
114#line 38
115    __cil_tmp12 = (List )0;
116#line 38
117    __cil_tmp13 = (unsigned int )__cil_tmp12;
118#line 38
119    __cil_tmp14 = (unsigned int )t;
120#line 38
121    if (__cil_tmp14 == __cil_tmp13) {
122      {
123#line 38
124      exit(1);
125      }
126    } else {
127
128    }
129    }
130#line 39
131    __cil_tmp15 = (unsigned int )p;
132#line 39
133    __cil_tmp16 = __cil_tmp15 + 4;
134#line 39
135    *((struct node **)__cil_tmp16) = t;
136#line 40
137    __cil_tmp17 = (unsigned int )p;
138#line 40
139    __cil_tmp18 = __cil_tmp17 + 4;
140#line 40
141    p = *((struct node **)__cil_tmp18);
142  }
143  while_0_break: /* CIL Label */ ;
144  }
145#line 42
146  *((int *)p) = 3;
147#line 45
148  p = a;
149#line 46
150  if (flag) {
151    {
152#line 47
153    while (1) {
154      while_1_continue: /* CIL Label */ ;
155      {
156#line 47
157      __cil_tmp19 = *((int *)p);
158#line 47
159      if (__cil_tmp19 == 1) {
160
161      } else {
162        goto while_1_break;
163      }
164      }
165#line 48
166      __cil_tmp20 = (unsigned int )p;
167#line 48
168      __cil_tmp21 = __cil_tmp20 + 4;
169#line 48
170      p = *((struct node **)__cil_tmp21);
171    }
172    while_1_break: /* CIL Label */ ;
173    }
174  } else {
175    {
176#line 50
177    while (1) {
178      while_2_continue: /* CIL Label */ ;
179      {
180#line 50
181      __cil_tmp22 = *((int *)p);
182#line 50
183      if (__cil_tmp22 == 2) {
184
185      } else {
186        goto while_2_break;
187      }
188      }
189#line 51
190      __cil_tmp23 = (unsigned int )p;
191#line 51
192      __cil_tmp24 = __cil_tmp23 + 4;
193#line 51
194      p = *((struct node **)__cil_tmp24);
195    }
196    while_2_break: /* CIL Label */ ;
197    }
198  }
199  {
200#line 52
201  __cil_tmp25 = *((int *)p);
202#line 52
203  if (__cil_tmp25 != 3) {
204    ERROR: 
205    goto ERROR;
206  } else {
207
208  }
209  }
210#line 54
211  return;
212}
213}
↑