1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
|
// CBMC reports a counterexample yet the assertion should hold
//
// Counterexample is not reported anymore when doing one or more of:
// - removing 'int value' from the struct node
// - replacing the malloc by static allocation
// - replacing the conditional in line 32 by 'hd = gl_list.next'
#include <assert.h>
struct list_head {
struct list_head *next;
};
struct node {
int value;
struct list_head linkage;
};
struct list_head gl_list;
int main()
{
// Create node
struct node *nd;
nd = (struct node *)__CPROVER_allocate(sizeof(struct node), 0);
// Link node
struct list_head *hd = &(nd->linkage);
gl_list.next = hd;
hd->next = &gl_list;
hd = (gl_list.next == &gl_list) ? 0 : gl_list.next; // always returns gl_list.next
// Delete node
hd = hd->next; // then: hd == &gl_list
hd->next = hd; // then: gl_list.next == &gl_list
// In the generated constraints, CBMC takes for the value of gl_list.next
// the value assigned in line 29. But gl_list.next is changed through a
// pointer in line 36.
assert(gl_list.next == &gl_list); // Holds
return 0;
}
|
