Showing error 1451

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

Source: 

 98#line 25
 99    *((struct node **)__cil_tmp10) = p;
100#line 26
101    p = t;
102  }
103  while_0_break: /* CIL Label */ ;
104  }
105  {
106#line 28
107  while (1) {
108    while_1_continue: /* CIL Label */ ;
109    {
110#line 28
111    __cil_tmp11 = (List )0;
112#line 28
113    __cil_tmp12 = (unsigned int )__cil_tmp11;
114#line 28
115    __cil_tmp13 = (unsigned int )p;
116#line 28
117    if (__cil_tmp13 != __cil_tmp12) {
118
119    } else {
120      goto while_1_break;
121    }
122    }
123    {
124#line 29
125    __cil_tmp14 = *((int *)p);
126#line 29
127    if (__cil_tmp14 != 1) {
128      ERROR: 
129      goto ERROR;
130    } else {
131
132    }
133    }
134#line 32
135    __cil_tmp15 = (unsigned int )p;
136#line 32
137    __cil_tmp16 = __cil_tmp15 + 4;
138#line 32
Show full sources
↑