--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on May 2012 ---
Hi, First, I have modified the function (see the function below). However, the VCs were not proved in the behavior 'one' (actually the VCs are not the same of previous function): 1.single_value (select(float_P_float_M_AB_Ptr_1,AB_Ptr))= single_value(select(float_P_float_M_AB_Ptr_1_0, AB_Ptr)) 2.single_value (select(float_P_float_M_AB_Ptr_2,CD_Ptr))= single_value(select(float_P_float_M_CD_Ptr_2_0, CD_Ptr)) 7.single_value (select(float_P_float_M_AB_Ptr_1,AB_Ptr))= single_value(select(float_P_float_M_AB_Ptr_1_0, AB_Ptr)) 8.single_value (select(float_P_float_M_CD_Ptr_2,CD_Ptr))= single_value(select(float_P_float_M_CD_Ptr_2_0, CD_Ptr)) @*/ extern double fabs(double x); #define LIMIT 6.111111e-2 /*@ requires \valid(AB_Ptr) && \valid(CD_Ptr); @ assigns *AB_Ptr; @ assigns *CD_Ptr; @ behavior zero: @ assumes \abs (\exact(*AB_Ptr)) > 5.235988e-2 || \abs (\exact(*CD_Ptr)) > 5.235988e-2; @ assigns *AB_Ptr; @ assigns *CD_Ptr; @ ensures \abs((\exact(*AB_Ptr)+ (5.235988e-2 - \exact(*AB_Ptr))) - 5.235988e-2) < 0.000000000000001; @ ensures \abs((\exact(*CD_Ptr)+ (5.235988e-2 - \exact(*CD_Ptr))) - 5.235988e-2) < 0.000000000000001; @ behavior one: @ assumes \abs((\exact(*AB_Ptr)+ (5.235988e-2 - \exact(*AB_Ptr))) - 5.235988e-2) < 0.000000000000001 && (\abs((\exact(*CD_Ptr)+ (5.235988e-2 - \exact(*CD_Ptr))) - 5.235988e-2) < 0.000000000000001); @ ensures \old(*AB_Ptr) == *AB_Ptr; @ ensures \old(*CD_Ptr) == *CD_Ptr; @ ensures \abs((\exact(*AB_Ptr)+ (5.235988e-2 - \exact(*AB_Ptr))) - 5.235988e-2) < 0.000000000000001; @ ensures \abs((\exact(*CD_Ptr)+ (5.235988e-2 - \exact(*CD_Ptr))) - 5.235988e-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); } } I didn?t understand why I need to put the assigns in the default behavior. What is the problem? Thanks. 2012/5/3 Lo?c Correnson <loic.correnson at cea.fr> > 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<Frama-c-discuss at lists.gforge.inria.fr> >> http://lists.gforge.inria.fr/**cgi-bin/mailman/listinfo/**frama-c-discuss<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss> >> > > > ______________________________**_________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.**inria.fr<Frama-c-discuss at lists.gforge.inria.fr> > http://lists.gforge.inria.fr/**cgi-bin/mailman/listinfo/**frama-c-discuss<http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss> > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120503/87982a0b/attachment.html>