--- layout: fc_discuss_archives title: Message 99 from Frama-C-discuss on October 2008 ---
Hi, You can mention any term inside construct \old, with the meaning that implicit parts of the states to interpret this term will be taken from the pre-state. What you need is a bit more complex, it requires that a predicate takes into two states, so that some of its sub-terms are evaluated in one state, and others subterms in another state. There is a construct in Frama-C that should be already supported by the Jessie plugin in the Helium release, to express such states: /*@ predicate is_permutation{S1,S2}(int *a, int *b, int s) = @ \forall integer k; @ 0 <= k < s ==> \at(a[k],S1) == \at(a[k],S2); @*/ /*@ ensures is_permutation{Here,Old}(a,a,s); @ */ void permut(int *a, int s); HTH, Yannick On Wed, Oct 22, 2008 at 8:08 AM, Christoph Weber < Christoph.Weber@first.fraunhofer.de> wrote: > Hi again, > > I wonder if it is somehow possible to refer to an array (not the elements) > in Pre state after the termination of a function. > e.g. > > /*@ > ... > ensures is_permutation (a, \old*_range*(a)); > */ > permutate(int* a); > > Otherwise I would have to write outrageous complex ensures clauses. > > Salut > > Christoph > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss@lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081022/1f6f25b7/attachment.html