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