--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on May 2012 ---
[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