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] Jessie - "No code for function <name>, default assigns generated"

On 10/27/10, Jens Gerlach <jens.gerlach at first.fraunhofer.de> wrote:
>
> Here is a simplified example for Kerstin's question (see the attached
> files).

I believe that the attached file further reduces the problem to its
simplest expression (but it was clear the first time in Kerstin's
message). You are observing a small misfeature. The attached file
contains the workaround: provide toplevel assigns for your function.

If I reduced the problem too much, then feel free to explain how the
original was different.

> Does the generated default assigns mean that everything may be modified?

Never rely on the default generated assigns, which will never mean
what you want because C uses pointers left and right for different
things. They cannot (or rather "should not", if I believe a recent BTS
entry) make a proof incorrect, because they must be checked for the
function and are then used for the calls. They will prevent your
verifications from working, however, either because they are too
strong to be proved for the function or too weak to provide the
necessary information in the callers.

> Is it bad practice and even dangerous to split assigns to the behaviors like
> in the example above?

No, it is neither dangerous nor bad practice. Just write a global
assigns clause that is the union of the sub-clauses in addition to the
behavior-specific assigns. Each behavior is supposed to hold
independently, so the provers will be able to use the more precise
assigns when they know the call is in a specific behavior (see
attached file).

Pascal
-------------- next part --------------
A non-text attachment was scrubbed...
Name: t.c
Type: application/octet-stream
Size: 448 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101028/cc4c0a3b/attachment.obj>