Frama-C Bug Tracking System - Frama-C
View Issue Details
0000927Frama-CPlug-in > sparecodepublic2011-08-17 18:142014-02-12 16:54
djs52 
Anne 
normalminoralways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000927: Sparecode could eliminate unnecessary if statements
This arose trying to use the [sparecode] plugin from another plugin, where constant propagation has reduced a conditional to "if (1)". However, a similar case from the command line is: int main (int x) { //@assert x>5; if (x > 5) { return 3; } else { return 4; } } # frama-c -sparecode-analysis /tmp/test.c ... /* Generated by Frama-C */ int main(int x ) { int __retres ; /*@ assert (x > 5); */ ; if (x > 5) { __retres = 3; } return (__retres); } Note that although [sparecode] has figured out that the else branch can be ignored, it has not removed the if condition, which is also redundant by the same reasoning.
No tags attached.
Issue History
2011-08-17 18:14djs52New Issue
2011-08-17 18:14djs52Statusnew => assigned
2011-08-17 18:14djs52Assigned To => Anne
2011-08-18 09:01AnneNote Added: 0002148
2011-09-21 10:30AnneNote Added: 0002303
2011-09-21 10:31svnCheckin
2011-09-21 10:35AnneStatusassigned => resolved
2011-09-21 10:35AnneResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0002148)
Anne   
2011-08-18 09:01   
I am wondering where is best place to decide that the condition must be marked as invisible so that [filter] remove it later on... It has to be done quiet early so that the dependencies of the condition are not selected to be visible. It could be done during the PDG computation, but it seems quiet strange to remove the dependency between an assignment [x = 10] and the condition [if (x > 5)]... I have to think a little more about that !
(0002303)
Anne   
2011-09-21 10:30   
This problem is solved now, but it might be worth mentioning that the [-val-signed-overflow-alarms] option helps to get better results on bigger examples.