Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000251Frama-CPlug-in > Evapublic2009-09-20 19:292014-02-12 16:58
Reporterpascal 
Assigned Toyakobowski 
PriorityimmediateSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000251: wrong origin displayed in the GUI
Description~/ppc/bin/viewer.opt -val imprecise.c

Inspect value of F at the last statement before return.
It shows Origin: Misaligned ..:19
This is correct (we are at line 19).
Inspect the value of "*p"
It shows Origin: Misaligned ..:20
This is incorrect. Line 20 has not even been analyzed yet.

Note: this is probably only a problem in display (since F is correct).
Unfortunately this happens in a demo I was planning to do soon for
someone that matters a lot. Quick fix very much appreciated if at all
possible (meanwhile I will try to hide the problem by adjusting
the demo).
TagsNo tags attached.
Attached Filesc file icon imprecise.c [^] (325 bytes) 2009-09-20 19:29 [Show Content]

- Relationships

-  Notes
(0000409)
pascal (reporter)
2009-09-20 19:37

Ok, I have understood the problem. The origin is incorrect when clicking *(expr) in the GUI because there is an evaluation caused by the click itself. I will work around it.
(0001905)
signoles (manager)
2011-05-16 17:30

The priority of this task is "immediate" since 1,5 year ;-). Are you sure that it is really the case?
(0003072)
yakobowski (manager)
2012-06-09 20:35

Value's GUI was not positioning Cil.currentLoc before evaluating *p. This is now fixed.
(0004672)
yakobowski (manager)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2009-09-20 19:29 pascal New Issue
2009-09-20 19:29 pascal Status new => assigned
2009-09-20 19:29 pascal Assigned To => pascal
2009-09-20 19:29 pascal File Added: imprecise.c
2009-09-20 19:37 pascal Note Added: 0000409
2011-03-30 18:38 pascal Relationship added related to 0000772
2011-05-16 17:30 signoles Note Added: 0001905
2012-06-09 20:35 yakobowski Note Added: 0003072
2012-06-09 20:36 svn Checkin
2012-06-09 20:36 svn Status assigned => resolved
2012-06-09 20:36 svn Resolution open => fixed
2012-06-09 20:40 yakobowski Relationship deleted related to 0000772
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:58 yakobowski Note Added: 0004672
2014-02-12 16:58 yakobowski Assigned To pascal => yakobowski
2014-02-12 16:58 yakobowski Status closed => resolved
2018-01-12 14:26 signoles Category Plug-in > value analysis => Plug-in > Eva


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker