Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000666Frama-CGraphical User Interfacepublic2011-01-11 13:392014-02-12 16:55
Reportersignoles 
Assigned Topascal 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Carbon-20110201 
Summary0000666: Wrong evaluation of expression in the GUI
DescriptionWhen evaluating an expression in the GUI, the result "After statement" seems to be equal to the result "Before statement" in some cases (e.g. if the statement is a conditional). Of course, that is incorrect in the general cases.
Steps To ReproduceConsider the following program:
==========
int t[2], c;
void main(void) {
  t[0] = 0;
  t[1] = 0;
  if (c) t[0] = 1; else t[0] = 2;
  t[1] += t[0];
}
==========

1) Run the GUI with options -val -lib-entry on this program.
2) Left-click at the end of the line containing "if". The information panel indicates that this line modifies t[0]: good.
3) Right-click at the end of the line containing "if" and select "Evaluate expression".
4) Enter "t[0]" as expression.
5) the information panel indicates that t[0] is equal to 0 after this statement. Quite bad, doesn't it?

Note: before statement "t[1] += t[0]", t[0] is 1 or 2: that is ok and that is the expected result after the conditional...
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001377)
signoles (manager)
2011-01-11 14:04

After Pascal explanations: no bug with the evaluation of the expression since the selected part is actually just the condition of the conditional if(c).

But, in this case, indicating that this selection modifies t[0] is wrong. There is still a bug somewhere ;-). And the highlighting is at least misleading...

- Issue History
Date Modified Username Field Change
2011-01-11 13:39 signoles New Issue
2011-01-11 13:39 signoles Status new => assigned
2011-01-11 13:39 signoles Assigned To => monate
2011-01-11 14:04 signoles Note Added: 0001377
2011-01-12 11:28 yakobowski View Status private => public
2011-01-12 11:29 signoles Assigned To monate => pascal
2011-01-12 11:29 signoles Product Version Frama-C GIT, precise the release id => Frama-C Carbon-20101202-beta2
2011-01-12 11:29 svn Checkin
2011-01-12 11:29 svn Status assigned => resolved
2011-01-12 11:29 svn Resolution open => fixed
2011-02-09 14:36 signoles Status resolved => closed
2011-02-09 14:37 signoles Fixed in Version => Frama-C Carbon-20110201


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker