 04 Sep, 2011 2 commits


Andrei Paskevich authored

MARCHE Claude authored

 03 Sep, 2011 2 commits


JeanChristophe Filliâtre authored

Guillaume Melquiond authored
Somehow they went under the radar the first time. Now all of them should have been fixed. Strangely enough, as can be seen from the diff, the statement of WP_parameter_gcd was thoroughly wrong. The old proof was actually matching the new statement, so the file would never have compiled on its own. I don't have any sensible explanation for such a breakage, except for gnomes messing with bytes at night.

 02 Sep, 2011 9 commits


Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Andrei Paskevich authored

Guillaume Melquiond authored
 "AltErgo 0.93"  "0.93.1"

 01 Sep, 2011 4 commits


Guillaume Melquiond authored

Guillaume Melquiond authored
I am assuming these numbers are not negative. This assumption has always existed for integers and the lexer cannot create negative real numbers anyway. So, as long as a transformation does not create negative numbers, there won't be any issue. (Transformations applying a negation to positive numbers are fine though.)

Guillaume Melquiond authored

Guillaume Melquiond authored

 31 Aug, 2011 2 commits


MARCHE Claude authored

Guillaume Melquiond authored
This is getting tedious. There should be a way to drop the content of a whole theory.

 29 Aug, 2011 1 commit


JeanChristophe Filliâtre authored

 25 Aug, 2011 1 commit


JeanChristophe Filliâtre authored

 24 Aug, 2011 2 commits


MARCHE Claude authored

MARCHE Claude authored
. but need further cleaning

 23 Aug, 2011 6 commits


Guillaume Melquiond authored

Guillaume Melquiond authored

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, ifthenelse, letin, 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 floatingpoint 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.111111e2; @ ensures \abs(*CD_Ptr) <= 6.111111e2; @ */ 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.111111e2) { *AB_Ptr = (float) (((*AB_Ptr) * 6.111111e2) / max); *CD_Ptr = (float) (((*CD_Ptr) * 6.111111e2) / max); } }

Guillaume Melquiond authored

Guillaume Melquiond authored
In particular, they are now sufficient to prove that the difference of two nonnegative floatingpoint numbers do not overflow.

Guillaume Melquiond authored

 22 Aug, 2011 9 commits


JeanChristophe Filliâtre authored

Guillaume Melquiond authored
Note that CVC3 doesn't care about syntax errors and it will still answer valid at the end. Currently, CVC3 chokes on the following kind of declarations (Div_mult, Abs_real_pos, and so on). ASSERT (FORALL (x : INT, y : INT, z : INT):PATTERN (div(((x * y) + z), x)): (((0 < x) AND ((0 <= y) AND (0 <= z))) => (div(((x * y) + z), x) = (y + div(z, x)))));

JeanChristophe Filliâtre authored

MARCHE Claude authored

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

JeanChristophe Filliâtre authored

MARCHE Claude authored

MARCHE Claude authored

 20 Aug, 2011 1 commit


Guillaume Melquiond authored
Modify the source buffer so that the filename is used for selecting syntax highlighting rather than always using why. This ensures that C files (coming from Jessie) are not uniformly blue due to pointer deferencing "(*ptr)". For unrecognized files (e.g. Jesse files), the IDE falls back to the old approach, that is, using Why highlighting.

 19 Aug, 2011 1 commit


JeanChristophe Filliâtre authored
