--- layout: fc_discuss_archives title: Message 59 from Frama-C-discuss on August 2015 ---
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>