Showing error 1392

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

Source: 

 1# 1 "files/oomInt.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/oomInt.c"
 5
 6
 7
 8  void assert(int i)
 9  {
10 if (i == 0)
11 {
12  ERROR: goto ERROR;
13 }
14  }
15# 20 "files/oomInt.c"
16
17
18
19int abs_int(int i)
20{
21 if (i < 0)
22 {
23
24
25  return -i;
26 }
27 else return +i;
28}
29int p = 0;
30void firstFunction()
31{
32 p = abs_int(-3);
33 assert(p >= 0);
34}
35
36void main()
37{
38 firstFunction();
39}
↑