--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on March 2010 ---
David Delmas wrote: > Sorry, my last message was sent unfinished : > > Le vendredi 12 mars 2010 ? 10:48 +0100, David Delmas a ?crit : > >> I don't know if it is any related, but I also just submitted a different >> Jessie crash <http://bts.frama-c.com/view.php?id=426>. >> > > I would be happy to be shown a work-around to avoid this #426 crash. > Indeed, it is blocking for my current experiments. > > Jessie does not like structures passed by value to logic functions and predicates. Please use extra pointers: typedef struct { int index; char b; } T_S; //@ predicate P0{L}(T_S *s) = (s->b==1) ; /*@ axiomatic Index { logic integer f_index{L}(integer old, T_S *new); // YYY ceci ne fait plus crasher Jessie :-) axiom Index1{L}: \forall integer old, T_S *new; P0{L}(new) ==> f_index{L}(old, new) == old; }*/ -- 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 |