2021-02-27 10:28 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000251Frama-CPlug-in > Evapublic2014-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)

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)

The priority of this task is "immediate" since 1,5 year ;-). Are you sure that it is really the case?

~0003072

yakobowski (manager)

Value's GUI was not positioning Cil.currentLoc before evaluating *p. This is now fixed.

~0004672

yakobowski (manager)

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