Skip to content

Wrong evaluation of expression in the GUI

ID0000666: This issue was created automatically from Mantis Issue 666. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0000666 Frama-C Graphical User Interface public 2011-01-11 2014-02-12
Reporter signoles Assigned To pascal Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Carbon-20101202-beta2 Target Version - Fixed in Version Frama-C Carbon-20110201

Description :

When 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 Reproduce :

Consider 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...

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information