Showing error 1366

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


Source:

 1# 1 "files/ex3_forlist.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/ex3_forlist.c"
 5# 1 "./assert.h" 1
 6
 7void __blast_assert()
 8{
 9 ERROR: goto ERROR;
10}
11# 2 "files/ex3_forlist.c" 2
12# 10 "files/ex3_forlist.c"
13
14
15
16
17void *pp[2];
18int pstate[2];
19
20void init() {
21 int i;
22 for(i=0; i<2; i++) {
23  pp[i]=0;
24  pstate[i]=0;
25 }
26}
27
28void f(void *pointer) {
29 int i;
30 for(i=0; i<2; i++) {
31  if(pp[i]==0) {
32   pp[i]=pointer;
33   pstate[i]=1;
34   break;
35  }
36 }
37}
38
39void g(void *pointer) {
40 int i;
41 for(i=0; i<2; i++) {
42  if(pp[i]==pointer) {
43
44   ((pstate[i]==1) ? (0) : __blast_assert ());
45   pstate[i]=2;
46  }
47 }
48}
49
50int counter = 1;
51void *malloc(int size) {
52 return counter++;
53
54}
55
56int main() {
57 int *a;
58 int *b;
59 init();
60 a = malloc(sizeof(int));
61 b = malloc(sizeof(int));
62 if(a==0 || b==0)
63  return -1;
64
65 f(a);
66 f(b);
67 g(a);
68
69 g(b);
70
71
72
73 return 0;
74}