Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie - behavior

  • Subject: [Frama-c-discuss] Jessie - behavior
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Fri, 22 Feb 2013 18:09:59 -0300
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>