--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on October 2013 ---
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>