--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on August 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Simplifying branches



On Mon, 2011-08-22 at 14:17 +0200, Julien Signoles wrote:
> Hello,
> 
> Le 17/08/2011 16:29, Daniel Sheridan a ?crit :
> > I am working on a plugin which eliminates branches of code under certain
> > circumstances. Using a combination of constant propagation and spare
> > code analysis, I end up with code of the form
> >
> >   if (1) {
> >      ...
> >   }
> >
> > which is technically correct, but would be more useful if it were
> > simplified. I notice that saving the code to disk and loading it in to
> > Frama-C is enough to eliminate the unnecessary "if".
> 
> If I well understand what you are saying, you pretty print the generated 
> code into a C file by using options "-print" and "-ocode", then you 
> re-execute Frama-c on this file. Is it correct?

Basically, yes, though it's all done in a plugin.

> > Is it possible to access this simplification step from a plugin, or do I
> > need to write my own visitor-based implementation of it?
> 
> In the next Frama-C version, there will be a function 
> File.create_rebuilt_project_from_visitor which will do the job [*].

That's exactly what I'm looking for. Thanks.

Would it be possible to access the Frama-C Subversion so that I can try
this out?

	Dan.