Showing error 1396

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


Source:

 1# 1 "files/recursive_list.c"
 2# 1 "<built-in>"
 3# 1 "<command-line>"
 4# 1 "files/recursive_list.c"
 5# 9 "files/recursive_list.c"
 6
 7typedef unsigned int size_t;
 8extern  __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__));
 9
10void err()
11{ ERROR: goto ERROR; }
12
13struct list {
14 int n;
15 struct list *next;
16};
17
18
19
20int i = 1;
21void * allocate_memory()
22{
23 return malloc(8U);
24}
25
26struct list* append(struct list *l, int n)
27{
28 struct list *new_el;
29
30 new_el = allocate_memory();
31
32 new_el->n = n;
33 new_el->next = l;
34
35 return new_el;
36}
37
38int main()
39{
40 struct list *l,m;
41 l = &m;
42 l->next = 0;
43 l->n = 0;
44
45 l = append(l, 1);
46 l = append(l, 2);
47
48
49
50
51 if (l->next->next->n == 0) err();
52
53
54}