--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on August 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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



>> 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