--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: Local variables leading to



Hi,

Changing the contract of my_changes into

/*@
  requires \valid(s);
  assigns s->i;
  ensures s->i == s->j;
*/

would probably be better. Generaly rule of thumb: Jessie does not 
support well direct structures,
it is better to mention only pointers to structures.

About the failure when separation analysis is on: yes, I'm afraid this 
analysis has bugs
when taking adresses of local variables.

- Claude

On 10/17/2010 06:35 PM, Pascal Cuoq wrote:
> #pragma SeparationPolicy(none)
>
> typedef struct _my_type {int i; int j;} my_type;
>
> /*@
>   requires \valid(s);
>   assigns (*s);
>   ensures s->i == \old(s->j);
> */
> void my_changes (my_type* s){s->i = s->j;};
>
> /*@
>   assigns \result;
>   ensures \result == n;
> */
> int my_main (int n){
>   my_type t;
>   t.j=n;
>   my_changes(&t);
>   return t.i;
> }
>    


-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |