Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000927Frama-CPlug-in > sparecodepublic2011-08-17 18:142014-02-12 16:54
Reporterdjs52 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000927: Sparecode could eliminate unnecessary if statements
DescriptionThis 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.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002148)
Anne (reporter)
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 (reporter)
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.

- Issue History
Date Modified Username Field Change
2011-08-17 18:14 djs52 New Issue
2011-08-17 18:14 djs52 Status new => assigned
2011-08-17 18:14 djs52 Assigned To => Anne
2011-08-18 09:01 Anne Note Added: 0002148
2011-09-21 10:30 Anne Note Added: 0002303
2011-09-21 10:31 svn Checkin
2011-09-21 10:35 Anne Status assigned => resolved
2011-09-21 10:35 Anne Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker