mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
059c2b5473
multi-lines spec comments /*@ ... */ axioms, with syntax //@ assume ...; assignments operators ++ -- += etc. for array elements
39 lines
602 B
C
39 lines
602 B
C
|
|
#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: */
|