Showing error 139

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_1.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 22 "files/oomInt.c"
15int abs_int(int i ) 
16{ 
17
18  {
19#line 24
20  if (i < 0) {
21#line 28
22    return (- i);
23  } else {
24#line 30
25    return (i);
26  }
27}
28}
29#line 32 "files/oomInt.c"
30int p  =    0;
31#line 33 "files/oomInt.c"
32void firstFunction(void) 
33{ 
34
35  {
36  {
37#line 35
38  p = abs_int(-3);
39  }
40#line 36
41  if (p >= 0) {
42
43  } else {
44    {
45#line 36
46    __blast_assert();
47    }
48  }
49#line 37
50  return;
51}
52}
53#line 39 "files/oomInt.c"
54int main(void) 
55{ 
56
57  {
58  {
59#line 41
60  firstFunction();
61  }
62#line 42
63  return;
64}
65}
↑