--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on August 2009 ---
sorry, I should have used struct pointers originally : struct stack { //@ ghost abstract_stack my_abstraction; } st; /*@ axiomatic A { @ logic integer count_of{L} (Stack *s) reads s->my_abstraction; @*/ /*@ requires 0 < count_of{Here}(st); @ assigns st.my_abstraction; @ ensures count_of{Here}(&st) == count_of{Old}(&st) - 1; @*/ void pop(void) Anyway, passing structures by value to a predicate deserves a better explaination in ACSL. At least, I'm sure that it does not work has intended with the Jessie plugin. - Claude BAUDIN Patrick wrote: > >>> /*@ requires 0 < count_of{Here}(st); >>> @ assigns st.my_abstraction; >>> @ ensures count_of{Here}(st) == count_of{Old}(\old(st)) - 1; >>> @*/ >>> >>> in fact, the labels {Here} and {Old} given to count_of are insignificant >>> >>> >> Wrong again. It is the \old(st) which is useless: st is not modified by >> the function so \old(st)==st. >> In the other hand, count_of{Old}(st) is a priori different from >> count_of{Here}(st) since count_of >> reads st.my_abstraction and this is said to be assigned. >> > I can't see is how you can > > @ assigns st.my_abstraction > and > > @ ensures \old(st)==st > > in a same specification ? > > Patrick. > > ------------------------------------------------------------------------ > > _______________________________________________ > 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 -- 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 |