• Guillaume Melquiond's avatar
    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);
       }
    }
    4d7dd217
instantiate_predicate.ml 3.4 KB