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] Checking for side-effects

  • Subject: [Frama-c-discuss] Checking for side-effects
  • From: dcok at grammatech.com (David Cok)
  • Date: Fri, 07 Feb 2014 09:58:22 -0500
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C7660449B5@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C7660449B5@Mail1.FCMD.local>
Isn't this what the 'assigns' clause is for?
As in

/*@
     requires global == dummy;

     behavior GLOBAL_BELOW_5:
       assumes global < 5;
       assigns global;
       ensures global == \old(global) + 1;
    
     behavior GLOBAL_ABOVE_5:
       assumes global > 5;
       assigns global;
       ensures global == \old(global) - 1;

     behavior GLOBAL_EQUAL_5:
       assumes global == 5;
       assigns \nothing;
  
     complete behaviors;
     disjoint behaviors;
*/

- David

On 2/6/2014 2:47 PM, Dharmalingam Ganesan wrote:
> Hi,
>
> Is there a way to specific "negative" behaviours, for example, no variable should be updated except the given variable.
>
> For example, for this little code, WP can able to prove all behaviours. That's great. But, I do not want any change in the state of the system except the "global" value. In this code, the dummy variable's state can also change, which is an undesirable side-effect (let's assume).
>
> For large and complex code, it appears specifying what is not allowed would also help to make sure implementation = specification.
>
> I looked into -deps option to Frama-c, it appears to list the dependencies for each variable, which is helpful, but it does not quite check for undesired state changes.
>
> Any comments?
> Dharma
>
>
> int global = 0;
> int dummy = 0;
>
> /*@
>      requires global == dummy;
>
>      behavior GLOBAL_BELOW_5:
>        assumes global < 5;
>        ensures global == \old(global) + 1;
>     
>      behavior GLOBAL_ABOVE_5:
>        assumes global > 5;
>        ensures global == \old(global) - 1;
>
>      behavior GLOBAL_EQUAL_5:
>        assumes global == 5;
>        assigns \nothing;
>   
>      complete behaviors;
>      disjoint behaviors;
> */
> void update()
> {
>     if(global < 5) {
>         global++;
>         dummy++;
>     }
>
>     if(global > 5) {
>         global--;
>         dummy--;
>     }
> }
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss