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] 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>