--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on February 2013 ---
Hi, I would like to confirm if my annotation is correct. The function1 is showed below. In the first called of function1 the status variable is equal FALSE. So, the value variable is equal 2 and it is possible to compute resultA variable. void function1(void) { if(status == FALSE) { status = TRUE; value = 2; } resultA = 50/value; } Without annotations, the VC about Check Division by zero is not proved (value <> 0). After a lot of tests, I have written behaviors that were proved: /* @ requires status == TRUE || FALSE; @ behavior ini: @ requires status == FALSE; @ behavior calc: @ requires status == TRUE; */ void function1(void) { if(status == FALSE) { status = TRUE; value = 2; } resultA = 50/value; } My doubts are: 1) The Check Division by zero VC was proved. Why this VC was proved with those annotations? 2) Im my first attempt to use behavior, I have written something like that (below). After, I noticed that is not necessary and only the @requires from behaviors were enough to prove. I could not understand. /*@ requires status == TRUE || FALSE; @ behavior ini: @ requires status == FALSE; @ assigns value; @ ensures value != 0; @ ensures status == TRUE; @ ensures resultA == 50/value; @ behavior calc: @ requires status == TRUE && value != 0; @ assigns resultA; @ ensures resultA == 50/value; */ Could you help me, please? Best regards, Rovedy -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130222/0852fe4e/attachment.html>