Showing error 146

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-regression/sizeofparameters_test.c-safe.cil.c
Line in file: 9
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 2 "./assert.h"
 5void __blast_assert(void) 
 6{ 
 7
 8  {
 9  ERROR:assert(0); 
10#line 4
11  goto ERROR;
12}
13}
14#line 5 "files/sizeofparameters_test.c"
15void foo(int a ) ;
16#line 7 "files/sizeofparameters_test.c"
17int globalSize  ;
18#line 9 "files/sizeofparameters_test.c"
19int main(int argc , char **argv ) 
20{ long a ;
21
22  {
23  {
24#line 12
25  globalSize = (int )4U;
26#line 13
27  foo(a);
28  }
29#line 14
30  return (0);
31}
32}
33#line 17 "files/sizeofparameters_test.c"
34void foo(int a ) 
35{ unsigned int __cil_tmp2 ;
36
37  {
38  {
39#line 18
40  __cil_tmp2 = (unsigned int )globalSize;
41#line 18
42  if (4U == __cil_tmp2) {
43
44  } else {
45    {
46#line 18
47    __blast_assert();
48    }
49  }
50  }
51#line 19
52  return;
53}
54}
↑