Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Help with proving post-conditions

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