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

  • Subject: [Frama-c-discuss] value analysis of function contain shift operations seems unable to stop
  • From: boris at yakobowski.org (Boris Yakobowski)
  • Date: Mon, 14 Oct 2013 12:57:07 +0200
  • In-reply-to: <CAA1cxugGNdnxaf25Z_z1XX9q=9B8QguzJ4OHkHZzBS6bFQDCBw@mail.gmail.com>
  • References: <CAA1cxugGNdnxaf25Z_z1XX9q=9B8QguzJ4OHkHZzBS6bFQDCBw@mail.gmail.com>
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