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