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] arbitrary buffers in analysis

On Fri, Aug 28, 2015 at 3:40 AM, Tim Newsham <tim.newsham at gmail.com> wrote:

>
>
> Using this driver -- plus option -memexec-all, which speeds things up
>> significantly -- the analysis takes 55 minutes and
>>
>
> Thank you.. this is exactly the type of feedback I was hoping for.
> One question: what is -memexec-all?  I see it mentioned briefly
> in the value help, but not in the frama-c manual.
>


Indeed, information about -memexec-all is rather scarce. But I'm giving a
talk about it in less than two weeks, so it was time to come out of hiding
:-)

This old post by Pascal explains its intents perfectly:

http://blog.frama-c.com/index.php?post/2012/09/21/A-value-analysis-option-to-reuse-previous-function-analyses

This option is not active by default in Frama-C for two reasons :
- it changes, sometimes significantly, the consolidated states on a given
statement. Those states are computed by Value and used by other plugins
such as PDG or Slicing. With -memexec-all, the values of the variables
never read or written by the function may no longer be proper
over-approximations, because of the executions that are skipped by the
analyzer.
- there remains a long-standing unsoundness for user-written ACSL
assertions that depend on those unread variables. This one will hopefully
be corrected in Frama-C Aluminium.

Still, none of Frama-C's existing plugins are impacted by the change of
semantics in the consolidated states, and the assertions that are analyzed
in an unsound way are extremely rare. I don't think I ever saw one written,
except in hand-crafted tests. So -memexec-all is almost always a safe bet.

The speedup can be considerable. On the industrial code for which this
technique was initially designed, the speedup is x46  (18 vs. 832). We
routinely achieve speedups on the order of magnitude of x20.

HTH,

-- 
Boris
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150828/837333cd/attachment.html>