--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on February 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - behavior



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>