--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] value analysis of function contain shift operations seems unable to stop



Dear Boris,

It helps a lot. Thank you very much. With this information, I can describe
why some functions that can't be analyzed within a given time.

I am looking forward to the Frama-C Neon version.

Besides, Is there any release time table for the new version? Or can we try
the development version?

Thanks again.

-david




On 14 October 2013 11:57, Boris Yakobowski <boris at yakobowski.org> wrote:

> Hi,
>
> The difficulty is not related to shifts, which are modeled precisely
> and efficiently by Value. On the other hand, the function 'hash' uses
> Duff's device [1], which contains a non-reducible loop. On such
> functions, Value will ultimately converge, but the convergence will be
> very slow. The development version for Frama-C Neon already improves
> support for non-reducible loops that contain an explicit loop
> construct (for, while, do while, i.e. all loops that are not
> completely encoded using gotos). This is the case for your example,
> which is analyzed instantly.
>
> [1] http://en.wikipedia.org/wiki/Duff%27s_device
>
> HTH,
>
>
> On Sun, Oct 13, 2013 at 2:37 AM, David Yang <abiao.yang at gmail.com> wrote:
> > Dear all,
> >
> > I only want to get pdg of this function. While I using frama-c to
> analysis
> > the function in the attached file, it seems that it always in the value
> > analysis state and never to stop anymore.
> >
> > The function in the attached file is not a large function. It only has
> about
> > 50 lines of code and does not call any other function.
> >
> > This is the following command for analysis the attached file:
> > frama-c -lib-entry -main hash hash.c -val -pdg -fct-pdg hash
> >
> > This function contains some shift operations. I don't know whether this
> is
> > the main reason.
> >
> > Thanks.
> >
> > Best regards,
> >
> > -David
> >
> >
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
>
>
> --
> Boris
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131014/e8bebffa/attachment.html>