Showing error 1394

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