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

[Frama-c-discuss] Simplifying branches



Le 17/08/2011 17:26, Daniel Sheridan a ?crit :
> Thanks for the pointer. As I am using sparecode as one of the steps in
> my plugin, I would expect to get this for free.

You are probably right !

> However, I see that
> optim_if is never called in such a way that it interprets constant 1 --
> it only eliminates the if statement if there is no condition, which
> seems to occur if the if statement itself is set to non-visible.

The visibility of the if statement in fact means the visibility
of the condition in this context, not the statements in the branches.

> I see that I could use the functor to get the result that I want. But I
> wonder whether this would be a useful enhancement, either in filter.ml
> or in sparecode?

Yes: [sparecode] should test whether the condition as a known value
(probably using [Db.Value.condition_truth_value]) to tell that the if statement
is invisible. I am wondering if it is a good idea or not to put that test
in [filter] since the "clients" of [filter] might want to keep the 'if',
don't they ?

Maybe you should add a feature request in Frama-C bug tracking system:
http://bts.frama-c.com/
to remind me to do that soon...

Thanks.
-- 
Anne.