0000666: Wrong evaluation of expression in the GUI

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000666

Frama-C

Graphical User Interface

public

2011-01-11 13:39

2014-02-12 16:55

Reporter

signoles

Assigned To

pascal

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Carbon-20101202-beta2

Target Version

Fixed in Version

Frama-C Carbon-20110201

Summary

0000666: Wrong evaluation of expression in the GUI

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

Tags

No 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