Frama-C-discuss mailing list archives

loic.correnson at cea.fr (Loïc Correnson) · Fri, 7 Feb 2014 16:45:29 +0100

Well,

There are complex issues on assigns clauses and behaviors. I?m not sure what is the default assigns clause when not all behaviors have some. Probably, assigns \everything, because this is the implicit one. I?m not convinced it is a good design choice, but ACSL manual is our only reference.

To specify your exclusion, a non-amibiguous specification can be:

/*@
  ?
  assigns global ; // Excludes any other variable, including dummy.
  behavior A:
      ? // No refinement, global can be modified.
  behavior B:
      assigns \nothing;  // Refinement, global can not be modified here !
*/

However, there is a known bug on WP with refined assigns on behaviors.
Hence, you should never use assigns clauses on behaviors. Try this:

/*@                                                                                                                                 
   requires global == dummy;                                                                                                        
   assigns global ;                                                                                                                 

   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;                                                                                                           
     ensures global == \old(global);                                                                                                

   complete behaviors;                                                                                                              
   disjoint behaviors;                                                                                                              
*/

There, you will find that the global assigns is not verified.
	L.

Le 7 f?vr. 2014 ? 16:12, Dharmalingam Ganesan <dganesan at fc-md.umd.edu> a ?crit :

> Hi,
> 
> In my understanding assigns clause is for ensuring the given variables are updated. If the code assigns additional variables that are not listed in the assign clause, then WP is not reporting as an issue. I understand that's ok, but my question is different: 
> 
> Can we specify only a given set of variables are allowed to be modified and nothing else?
> 
> Of course, for small programs we can add additional constraints such as dummy == \old(dummy), for example. But this workaround becomes an issue if the code has "too many" variables, we have to manually add such constraints for each variable that should not be modified.
> 
> Thanks,
> Dharma
> 
> -----Original Message-----
> From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David Cok
> Sent: Friday, February 07, 2014 9:58 AM
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [Frama-c-discuss] Checking for side-effects
> 
> 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://cp.mcafee.com/d/avndy0Od20Qrhpd7a8VVZ55MTsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdA3hOMWMWC_R-p79L3HZuVtdCUXDNP1EVupVqWdAklkkk-l3PWApmU6CQjqpK_8I9LfzAm4PhOrKr01DOFeD4ng0fZa4prPIs0gKgB31dnoovaAVgtHzItlQLoKxaBCWkdKNRniZyW4GmrFgKgGT2TQ1hYGjFN5Q03_ix6mYX4S-qekhNI5-Aq83iSbNRniZyW4GmrFgQKCy0i9_oHa14QgeRyq8aigYLXHLSDgSMedSnK1T1nG
> 
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://cp.mcafee.com/d/k-Kr3x8SyOqekhPPWabxKVJeXObP33WapJeXObP33Xz9JeXObP33Wb1JeXOrBS4TAPq17ovjo0FSNtl3CRkeZ1ISXoKGxPqG7uwSr86zBxRxRd_HYOeju7nWZOWrdNTfzC3hOYPORQr8EGEEFYG7DR8OJMddFCQPt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JYQsEzzobZ8Qg6BInzGKBX5Q9kITixFtd40Aj-Nmk29EwtH4QgkAxVvTnvJexJwsrhs5CczSf
> 
> _______________________________________________
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140207/466ed9b9/attachment-0001.html>