--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2009 ---
>> /*@ 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. -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090825/a0466ec5/attachment.htm