--- layout: fc_discuss_archives title: Message 97 from Frama-C-discuss on October 2008 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081022/27789efc/attachment.html