--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on December 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with ACSL annotations



Hello all,

I am a new user of frama-c.
I would like to verify this function:

/*@ requires \valid_range(queue,0,14);
??? ensures \result==0 ==> (\exists int i;0<=i<15 && ((\forall int j; 0<=j<15 && queue[i] > queue[j] )&&((queue[i]>=5) || (queue[i]<=10))));
*/
int find_array_max(int queue[15]){

? int i, largest;

? largest = 0;
/*@ loop variant 15 - i;
??? loop invariant 0 <= i <= 15;
??? 
*/
? for (i = 0; i < 15; i++) {
??? if (queue[i] > largest)
????? largest = queue[i];
? }
? 
? if ( (largest >= 5) || (largest <= 10) ) {
??? 
??? ? return 0;
? }

? return largest;

}

I had some problems to write postconditions in ACSL for this function.
Could you, please help me?

Best regards,
Intissar Mzalouat
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121218/c8e5064b/attachment.html>