GitLab

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