-
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); } }
4d7dd217