--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on February 2013 ---
Hello, I have a function that use static variables (attached file). In the first step of my verification (safety verification), I have obtained 4 Vcs not proved related to: - offset_min(float_P_acel_2_alloc_table, acel) <=i - i <= offset_max(float_P_acel_2_alloc_table, acel) - offset_min(float_P_acel_2_alloc_table, acel) <=i - i <= offset_max(float_P_acel_2_alloc_table, acel) In the ACSL manual, I have found a example related to the use of a data invariant on a local static variable. I am using the Carbon version and it is not possible to prove this example. void out_char (cha r c) { static int col = 0; //@ global invariant I : 0 <= col <= 79; col ++; i f ( col >= 80) col = 0; } Browsing in the web, I have found information that Jessie could not prove this kind of annotation: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-December/002920.html My doubts are: 1) I have read about solutions related to weak and strong invariants. In my function, I need to study those solutions or there is another simpler solution? 2) After the safety verification, I have tried to do the functional verification. I have written a pos-condition that test the static variable average like that: @ ensures (average > 5.0) ==> (G_E[A].G_Ativo == TRUE); But when I have tried to run, I have received this message: xx.c:19:[kernel] user error: unbound logic variable average in annotation. Is it wrong to use the "average" static variable in a pos-condition? Thanks a lot! Best regards, Rovedy #pragma JessieIntegerModel(math) #pragma JessieTerminationPolicy(user) #pragma JessieFloatModel(math) struct { unsigned int G_Ativo :1, G_Tratado :1; float G_Inst_Ativ; } G_E[61]; float Voo_Acel; /*@ ensures (average > 5.0) ==> (G_E[9].G_Ativo == 1); */ void calc() { static float average, acel[3], add; static unsigned char pri, i, j; if((G_E[7].G_Ativo == 1 && G_E[7].G_Ativo == 0)) { pri = 0; i = 0; add = 0; } acel[i] = Voo_Acel; i = i + 1; if (i > 3 - 1) { i = 0; pri = 1; } if (pri == 1) { add = 0; /*@ loop invariant 0 <= j <= 3 ; */ for(j=0;j<3;j++) add = add + acel[j]; average = add / 3.0; if(G_E[9].G_Ativo == 0) if(average > 5.0) G_E[9].G_Ativo = 1; } } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130217/ad091e24/attachment.html>