--- layout: fc_discuss_archives title: Message 56 from Frama-C-discuss on October 2010 ---
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 |