Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Use of Jessie and Value Analysis plug-in

  • Subject: [Frama-c-discuss] Use of Jessie and Value Analysis plug-in
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Fri, 19 Aug 2011 19:00:24 -0300
  • In-reply-to: <1313705735.1903.6.camel@guillaume-laptop>
  • References: <CAEtoXR2yzkk9sKSa4gy+7hAAQwWNZAZGXDQe+5Py94BS1tcLog@mail.gmail.com> <1313705735.1903.6.camel@guillaume-laptop>
>> Jessie 1) I have installed the Alt-Ergo 0.91, Simplify 1.5.4, Yices
>> 1.0.29, CVC3 2.2., and Gappa 0.15.0.
>> My first problem was a short function responsible by limiting a value
>> in an interval ?6.111111e-2 to +6.111111e-2
>> I created the annotation below but I didn?t get prove. The code is
>> showed below. I don?t know what I am doing wrong.
>>
>> /*@ requires \valid(AB) && \valid(CD);
>> ? @ assigns *AB_Ptr, *CD_Ptr;
>> ? @ ensures \abs(-6.111111e-2) <= *AB <= \abs(6.111111e-2);
>> ? @ ensures \abs(-6.111111e-2) <= *CD <= \abs(6.111111e-2);
>> ? @ */
>
> Note that you are trying to prove that *AB and *CD are exactly equal to
> 6.111111e-2, which is always false! So it's a good thing you were not
> able to prove it. Get rid of the \abs expressions.


1) Sorry for my mistake. I am sending the function with the new
annotations (2 versions) but the VCs related with ensures
clauses aren't proved.

/*@ assigns \nothing;
  @*/
extern double fabs(double) ;

#define LIMIT    6.111111e-2

 #pragma JessieFloatModel(defensive)

/*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
  @ assigns *AB_Ptr, *CD_Ptr;
  @ ensures -6.111111e-2 <= *AB_Ptr <= 6.111111e-2;
  @ ensures -6.111111e-2 <= *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 > LIMIT)
   {
      *AB_Ptr = (float) (((*AB_Ptr) * LIMIT) / max);
      *CD_Ptr = (float) (((*CD_Ptr) * LIMIT) / max);
   }
}

And another alternative is:

/*@ 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;
  @ */


Neither annotations works.  Can you help me?


>> Jessie 2) in another function, with a high number of computations (12
>> ifs, 28 assignments, 1 loop, 21 pointers accesses.)
>> The Jessie generated 2725 VCs for the safety checking. Is it normal?
>> It is appropriate to evaluate this function with Jessie? ?(Because the
>> computer is not a god machine I checked only one part #264).
>
> The following option might help you:
>
> ? ?frama-c -jessie -jessie-why-opt=--fast-wp <file.c>
>
> VCs won't get simpler and more easily provable, but at least there
> should be less of them.


2) I have gotten with this option 7 default behavior and 145 safety
Vcs against 669 default behavior and 2725 safety cheking.
I think that I will use this option.


I'm very grateful for the help

Best regards,
Rovedy