Showing error 138

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/oomInt.c-safe.cil.c
Line in file: 11
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 4 "files/oomInt.c"
 5void assert(int i ) 
 6{ 
 7
 8  {
 9#line 6
10  if (i == 0) {
11    ERROR:assert(0); 
12#line 8
13    goto ERROR;
14  } else {
15
16  }
17#line 10
18  return;
19}
20}
21#line 22 "files/oomInt.c"
22int abs_int(int i ) 
23{ 
24
25  {
26#line 24
27  if (i < 0) {
28#line 28
29    return (- i);
30  } else {
31#line 30
32    return (i);
33  }
34}
35}
36#line 32 "files/oomInt.c"
37int p  =    0;
38#line 33 "files/oomInt.c"
39void firstFunction(void) 
40{ int __cil_tmp1 ;
41
42  {
43  {
44#line 35
45  p = abs_int(-3);
46#line 36
47  __cil_tmp1 = p >= 0;
48#line 36
49  assert(__cil_tmp1);
50  }
51#line 37
52  return;
53}
54}
55#line 39 "files/oomInt.c"
56void main(void) 
57{ 
58
59  {
60  {
61#line 41
62  firstFunction();
63  }
64#line 42
65  return;
66}
67}
↑