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
|
#include <stdio.h>
#include <stdlib.h>
//@ function int x();
//@ assume x() < 2;
int foo(int a[]) {
//@ requires length(a) >= 1; ensures a[0] == old(a[0]);
a[0] /= 1;
}
int main()
{
int x = 42;
//@ label L;
//@ assert x == 42;
x = x+1;
//@ assert at(x, L) == 42;
while (x > 0) {
//@ invariant x >= 0;
//@ variant x;
x--;
}
//@ assert x == 0;
int a[10];
a[0] = 41;
//@ label ICI;
foo(a);
//@ assert a[0] == 42;
//@ assert at(a[0], ICI) == 41;
}
/* Local Variables: */
/* compile-command: "make -C ../.. && why3 prove -P alt-ergo test.c" */
/* End: */
|
