--- layout: fc_discuss_archives title: Message 90 from Frama-C-discuss on December 2009 ---
Hello, > ensures strlen(s) == strlen(\at(s, Old)) + strlen(append); Which strlen function are you trying to use here? If you mean the C function, you can't: it is not allowed to call a C function from inside a predicate such as a pre/prost-condition. You can have a logic function (I would recommend to use a slight variation on the strlen name), defined by yourself as the function that computes the length of a string. That is the right way to do it. Another thing: \at(s, Old) (that you can write \old(s)) does not do what you think it does. In fact, since strcat does not (in general, unless the caller created some strange aliasing conditions) modify its argument s, \old(s) is the same as s. What the logic function logic_strlen really takes in argument is a pointer s *and* a memory state in which s points to some bytes, and with this information, it is able to tell you what the length of s is *in the memory state that you provided*. Function logic_strlen only needs one memory state, so this memory state can remain implicit in the body of the definition, but you have to be aware that it is an argument of the function, and that you need to pass it. In this case you would pass Old i.e. write something like logic_strlen{Old}(s) instead of strlen(\at(s, Old)). Perhaps the explanations in chapter 8 of the ACSL mini-tutorial http://frama-c.cea.fr/download/acsl-tutorial.pdf can be of help. Pascal -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? enlev?e... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091209/3a8a3383/attachment.htm