--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on May 2012 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120502/94ea3f55/attachment.html>