--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on November 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"



Hello,
  Since your behaviors are completes and each of them has an assigns clause,
  the kernel of Frama-C shouldn't generate any more assigns.
  The generation of default assigns for function foo can be considered 
as a bug.
  Feels free to add it into the BTS of Frama-C.
Regards,
Patrick

-- 
Patrick Baudin,
CEA, LIST, DILS, F-91191 Gif-sur-Yvette cedex, France.
tel: +33 (0)1 6908 2072

>
> Here is a simplified example for Kerstin's question (see the attached 
> files).
> When I call
>
>     frama-c -jessie bar.c
>
> the I get (among others) the message
>
>    [kernel] No code for function foo, default assigns generated
>
> Is this message to be interpreted as a warning?
> Can anything go wrong if ignore this message?
>
> Regards
>
> Jens
>