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] Jessie plugin

Hi,
Maybe the problem comes from the different assigns clauses in each  
behavior (to be confirmed).
You may try the following :
  - put the weaker assigns clauses in default behavior  (assigns  
*AB_Ptr, *CD_ptr)
  - in behavior "one", turn the assign-nothing clause into ensures  
\old(*AB_Ptr) = *AB_ptr (resp. CD_Ptr)
Regards,
	L.


Le 2 mai 12 ? 21:14, Rovedy Aparecida Busquim e Silva a ?crit :

> Hi,
>
> I am studying Frama-C with a real case study. I have some questions  
> about Jessie.
> The Alt-Ergo 0.91, Simplify 1.5.4, Z3 2.19, CVC2.2, and Gappa 0.15.0  
> are installed.
>
> //  
> -------------------------------------------------------------------------------------------------------------
> 1) I would like to use behavior specification (see the function  
> below). But I couldn?t prove the Vcs
> related with the behavior one:
>
> 3 - not_assigns(float_P_AB_Ptr_1_alloc_table,  
> float_P_float_M_AB_Ptr_1,float_P_float_M_AB_Ptr_1_0, pset_empty)
> 4 - not_assigns(float_P_CD_Ptr_2_alloc_table,  
> float_P_float_M_CD_Ptr_2,float_P_float_M_CD_Ptr_2_0, pset_empty)
> 11- not_assigns(float_P_AB_Ptr_1_alloc_table,  
> float_P_float_M_AB_Ptr_1,float_P_float_M_AB_Ptr_1_0, pset_empty)
> 12- not_assigns(float_P_CD_Ptr_2_alloc_table,  
> float_P_float_M_CD_Ptr_2,float_P_float_M_CD_Ptr_2_0, pset_empty)
>
> I didn't understand the problem. If I don?t use behavior , I have  
> all the proven VCs.
>
>
> /*@ assigns \nothing;
>   @ ensures \result == \abs(x);
> @*/
> extern double fabs(double x);
>
> #define LIMIT 6.111111e-2
>
> /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
> @ behavior zero:
>     @ assumes \abs (\exact(*AB_Ptr)) > 6.111111e-2 || \abs  
> (\exact(*CD_Ptr)) > 6.111111e-2;
>     @ assigns *AB_Ptr;
>     @ assigns *CD_Ptr;
>     @ ensures  \abs((\exact(*AB_Ptr)+ (6.111111e-2 -  
> \exact(*AB_Ptr))) - 6.111111e-2) < 0.000000000000001;
>     @ ensures  \abs((\exact(*CD_Ptr)+ (6.111111e-2 -  
> \exact(*CD_Ptr))) - 6.111111e-2) < 0.000000000000001;
> @ behavior one:
>     @ assumes \abs((\exact(*AB_Ptr)+ (6.111111e-2 -  
> \exact(*AB_Ptr))) - 6.111111e-2) < 0.000000000000001 &&
>           (\abs((\exact(*CD_Ptr)+ (6.111111e-2 - \exact(*CD_Ptr))) -  
> 6.111111e-2) < 0.000000000000001);
>     @ assigns \nothing;
>     @ ensures  \abs((\exact(*AB_Ptr)+ (6.111111e-2 -  
> \exact(*AB_Ptr))) - 6.111111e-2) < 0.000000000000001;
>     @ ensures  \abs((\exact(*CD_Ptr)+ (6.111111e-2 -  
> \exact(*CD_Ptr))) - 6.111111e-2) < 0.000000000000001;
> @ */
> 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);
>     }
> }
>
> The function without behavior:
>
> /*@ assigns \nothing;
>   @ ensures \result == \abs(x);
> @*/
> extern double fabs(double x);
>
> #define LIMIT 6.111111e-2
>
> /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr);
>   @ assigns *AB_Ptr;
>   @ assigns *CD_Ptr;
>   @ ensures  \abs((\exact(*AB_Ptr)+ (6.111111e-2 - \exact(*AB_Ptr)))  
> - 6.111111e-2) < 0.000000000000001;
>   @ ensures  \abs((\exact(*CD_Ptr)+ (6.111111e-2 - \exact(*CD_Ptr)))  
> - 6.111111e-2) < 0.000000000000001;
>  */
> 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);
>     }
> }
>
> //-------------------------------------------------------------------------------------------------------------
>
> 2) How do I write a specification to verify the validity of pointer  
> to an array of structure?
>
> Example:
> filter *filter_Ptr[3];
>
> typedef struct
> {  float F_K;
>    float F_A;
>    float F_B1;
> } filter;
>
> The variable filter_Ptr is global.
>
>
> //-------------------------------------------------------------------------------------------------------------
>
> 3) How do I write a requires and assigns specification for a two- 
> dimensional array?
>
> //-------------------------------------------------------------------------------------------------------------
>
> 4) I have a function responsible for initializing values. It has no  
> input parameters. All variables used in the function are global.
> In this case, should I put as a pre condition to the validity of  
> pointers and arrays?
>
> //-------------------------------------------------------------------------------------------------------------
>
> 5) In the previous function, I would like to write assigns  
> specifications. However, the VCS aren?t proved.
> The variables are global. what is the problem?
>
> Example:
>
> float Pane [7];
> unsigned Sc [7] [3];
> float * Tab__Ptr[9];
> filter * filter_Ptr[3];
>
>
> /* @ assigns Pane[0 .. 7-1];
>   @ assigns Tab_Ptr[0 .. 9-1];
>   @ assigns filter_Ptr[0 .. 3-1];
>  */
>
> //-------------------------------------------------------------------------------------------------------------
> 6) Is there a way to count the number of VCs generated by type (eg  
> 188 poscondition, 50 precondition ...) without being visually?
> I searched this information in the directory files generated by  
> jessie but not found.
>
>
> Thanks a lot.
>
> Best regards,
> Rovedy
>
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss