MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

1. 18 Jul, 2012 1 commit
2. 20 Jun, 2012 1 commit
3. 18 Jun, 2012 1 commit
4. 17 Mar, 2012 1 commit
5. 24 Nov, 2011 1 commit
6. 13 Sep, 2011 1 commit
7. 23 Aug, 2011 2 commits
• Add a new transformation that instantiates the axioms marked with the · 4d7dd217
Guillaume Melquiond authored
```meta "instantiate : auto" on as many terms as possible.

The transformation is rather naive, since it doesn't look for term
candidates under quantifiers, if-then-else, let-in, and so on. So it can
only appear late in the transformation pipe.

It is only enabled for Gappa and its target axioms are the ones that state
that any floating-point value is bounded. It was the last transformation
from Why2 still missing in Why3.

Thanks to this transformation, Gappa is now able to prove all the safety
obligations from the following code, including the ones about division and
downcast, which is definitely frightening.

/*@ assigns \nothing;
@ ensures \result == \abs(x);
@*/
extern double fabs(double x);

/*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
@ assigns *AB_Ptr, *CD_Ptr;
@ ensures \abs(*AB_Ptr) <= 6.111111e-2;
@ ensures \abs(*CD_Ptr) <= 6.111111e-2;
@ */
void limitValue(float *AB_Ptr, float *CD_Ptr)
{
double Fabs_AB, Fabs_CD;
double max;

Fabs_AB = fabs (*AB_Ptr);
Fabs_CD = fabs (*CD_Ptr);

max = Fabs_AB;
if (Fabs_CD > Fabs_AB)  max = Fabs_CD;

if ( max > 6.111111e-2)
{
*AB_Ptr = (float) (((*AB_Ptr) * 6.111111e-2) / max);
*CD_Ptr = (float) (((*CD_Ptr) * 6.111111e-2) / max);
}
}```
8. 29 Jun, 2011 1 commit
9. 03 Jun, 2011 1 commit
10. 22 May, 2011 1 commit
11. 19 Apr, 2011 2 commits
12. 12 Apr, 2011 7 commits
13. 18 Mar, 2011 1 commit
14. 16 Mar, 2011 1 commit
15. 24 Jan, 2011 1 commit
16. 21 Jan, 2011 1 commit
17. 17 Dec, 2010 1 commit
18. 16 Dec, 2010 1 commit
19. 26 Nov, 2010 1 commit
20. 24 Nov, 2010 2 commits
21. 23 Nov, 2010 3 commits
22. 19 Nov, 2010 1 commit
23. 16 Sep, 2010 1 commit
24. 15 Sep, 2010 1 commit
25. 14 Sep, 2010 1 commit
26. 13 Sep, 2010 1 commit
27. 10 Sep, 2010 2 commits
28. 09 Sep, 2010 1 commit