--- layout: fc_discuss_archives title: Message 70 from Frama-C-discuss on October 2010 ---
[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>