File: main.c

package info (click to toggle)
cbmc 5.10-5
  • links: PTS
  • area: main
  • in suites: buster
  • size: 73,416 kB
  • sloc: cpp: 264,330; ansic: 38,268; java: 19,025; python: 4,539; yacc: 4,275; makefile: 2,547; lex: 2,394; sh: 932; perl: 525; xml: 289; pascal: 169
file content (60 lines) | stat: -rw-r--r-- 1,397 bytes parent folder | download | duplicates (10)
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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
// from SV-COMP, based on code found in the Linux kernel

#include <stdlib.h>

struct list_head {
	struct list_head *next, *prev;
};

struct node {
    int                         value;
    struct list_head            linkage;
    struct list_head            nested;
};

struct list_head gl_list = { &gl_list, &gl_list };

int main()
{
  _Bool maybe_dynamic;

  struct node X;
  struct node *N = maybe_dynamic ? malloc(sizeof(struct node)) : &X;
  if (!N)
    return 1;

  N->value = 42;
	gl_list.prev=&N->linkage;
	N->linkage.next=&gl_list;
	N->linkage.prev=&gl_list;
	gl_list.next=&N->linkage;
  // we have:
  // gl_list.prev=&D->linkage;
  // D->linkage.next=&gl_list
  // D->linkage.prev=&gl_list;
  // gl_list.next=&D->linkage;

	N->nested.next = &(N->nested);
  N->nested.prev = &(N->nested);

  const struct list_head *head=&gl_list;

  // go one step backward
  head = head->prev;
  // we have:
  // head=&D->linkage

  // resolve root
  const struct node *node =
    (struct node *) ((char *)(head) -
                     (unsigned long)(&((struct node *)0)->linkage));
  // we have:
  // node=&D (==&D->value)
  __CPROVER_assert(node == N, "");
  __CPROVER_assert(head == N->linkage.next->prev, "");
  __CPROVER_assert(head == N->linkage.prev->next, "");
  __CPROVER_assert(head == node->linkage.next->prev, "");
  __CPROVER_assert(head == node->linkage.prev->next, "");

  return 0;
}