Frama-C Bug Tracking System - Frama-C
View Issue Details
0000666Frama-CGraphical User Interfacepublic2011-01-11 13:392014-02-12 16:55
Assigned Topascal 
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

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
2011-01-11 13:39signolesNew Issue
2011-01-11 13:39signolesStatusnew => assigned
2011-01-11 13:39signolesAssigned To => monate
2011-01-11 14:04signolesNote Added: 0001377
2011-01-12 11:28yakobowskiView Statusprivate => public
2011-01-12 11:29signolesAssigned Tomonate => pascal
2011-01-12 11:29signolesProduct VersionFrama-C GIT, precise the release id => Frama-C Carbon-20101202-beta2
2011-01-12 11:29svn
2011-01-12 11:29svnStatusassigned => resolved
2011-01-12 11:29svnResolutionopen => fixed
2011-02-09 14:36signolesStatusresolved => closed
2011-02-09 14:37signolesFixed in Version => Frama-C Carbon-20110201
2013-12-19 01:12yakobowskiSource_changeset_attached => framac master 5804864d
2014-02-12 16:55yakobowskiSource_changeset_attached => framac stable/neon 5804864d