--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on December 2012 ---
Hello all, I am a biginner user of Frama-C. I need to verify this function using the jessie plug in. int find_largest(struct *queue, int nr_of_elements) { ? int i, largest; ? largest = 0; ? for (i = 0; i < nr_of_elements; i++) { ??? if (queue[i].p > largest) ????? largest = queue[i].p; ? } ? ? if ( (largest >= 10) ) { ??? ??? ? return 0; ? } ? return largest; } I got some problems to specify in ACSL this function because of the largest variable. Could you help me please? Best regards, Intissar -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20121210/55dd5093/attachment.html>