2021-02-27 10:28 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000251Frama-CPlug-in > Evapublic2009-09-20 19:292014-02-12 16:58
Reporterpascal 
Assigned Toyakobowski 
PriorityimmediateSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon imprecise.c (325 bytes) 2009-09-20 19:29 - 
    int *t[5];

int A[2],B,C,D,E,F,*p;

int unknownfunction(void);

int main()
{
  t[0] = A;
  t[unknownfunction()] = &B;
  *(t[0]) = 1;
  *(t[unknownfunction()]) = 2;

  *(int**) ((int)t+unknownfunction()) = &C;
  *(t[unknownfunction()]) = 3;
  E = 4;
  A[0] = (int) &D;
  p = t[unknownfunction()];
  F = *p + 12;
  return F;
}
    c file icon imprecise.c (325 bytes) 2009-09-20 19:29 +

-Relationships
+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.
+Notes

-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
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
2013-12-19 01:11 yakobowski Source_changeset_attached => framac master 0c565c3f
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon 0c565c3f
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
+Issue History