File: main.c

package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36
file content (50 lines) | stat: -rw-r--r-- 810 bytes parent folder | download 
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
 
#include <assert.h>
#include <stdlib.h>

typedef struct
{
  int *n;
} s;

void main()
{
  int *x1, y1, z1;
  x1 = &z1;

  while(y1 > 0)
    __CPROVER_loop_invariant(y1 >= 0 && *x1 == __CPROVER_loop_entry(*x1))
    {
      --y1;
      *x1 = *x1 + 1;
      *x1 = *x1 - 1;
    }
  assert(*x1 == z1);

  int x2, y2, z2;
  x2 = z2;

  while(y2 > 0)
    __CPROVER_loop_invariant(y2 >= 0 && x2 == __CPROVER_loop_entry(x2))
    {
      --y2;
      x2 = x2 + 1;
      x2 = x2 - 1;
    }
  assert(x2 == z2);

  int y3;
  s s0, s1, *s2 = &s0;
  s0.n = malloc(sizeof(int));
  s2->n = malloc(sizeof(int));
  s1.n = s2->n;

  while(y3 > 0)
    __CPROVER_loop_invariant(y3 >= 0 && s2->n == __CPROVER_loop_entry(s2->n))
    {
      --y3;
      s0.n = s0.n + 1;
      s2->n = s2->n - 1;
    }

  assert(*(s1.n) == *(s2->n));
}