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