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
61
62
63
64
65
66
|
/**************************************************************************/
/* */
/* The Why platform for program certification */
/* Copyright (C) 2002-2008 */
/* Romain BARDOU */
/* Jean-Franois COUCHOT */
/* Mehdi DOGGUY */
/* Jean-Christophe FILLITRE */
/* Thierry HUBERT */
/* Claude MARCH */
/* Yannick MOY */
/* Christine PAULIN */
/* Yann RGIS-GIANAS */
/* Nicolas ROUSSET */
/* Xavier URBAIN */
/* */
/* This software is free software; you can redistribute it and/or */
/* modify it under the terms of the GNU General Public */
/* License version 2, as published by the Free Software Foundation. */
/* */
/* This software is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. */
/* */
/* See the GNU General Public License version 2 for more details */
/* (enclosed in the file GPL). */
/* */
/**************************************************************************/
/*@ axiom A : \forall double t[]; \forall int i; \valid(t+i) => t[i]>0.0 => t[i]>=0.0 */
typedef struct U { int t2[5]; int t2bis[5]; int *p2; } las2;
typedef struct V { int t1[5]; int t1bis[5]; int *p1; las2 * pp; } las;
las u,v,w;
las2 z;
las2 y1[5];
las2 y2[10];
/* predicate separation_intern_struct_U(las2* p) reads p->t2, p->t2bis */
/* axiom sep_U :
\forall las2 *p; \valid(p) => separation_intern_struct_U(p) */
/*@ requires \valid(x) */
void f(struct U *x) { x->t2[0] = 1; *u.p1 = 1; *z.p2 = 2; }
int ff(double a,double b)
{
int x;
x=(a<b);
return x;
}
//@ ensures \result < a
double f2(double a) { return (a - 1.2e-3); }
/*@ requires 0.0 < x <= 1.0
*/
void f3(double x)
{
/* ... */
x = x * 2.0;
/* ... */
}
|
