Showing error 1447

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_safe.cil.c
Line in file: 205
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC

Source: 

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