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

[Frama-c-discuss] Help to write the specification in ACSL



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>