0000251: wrong origin displayed in the GUI - Frama-C Bug Tracking System

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

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0000251

Frama-C

Plug-in > Eva

public

2009-09-20 19:29

2014-02-12 16:58

Reporter

pascal

Assigned To

yakobowski

Priority

immediate

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Beryllium-20090901

Target Version

Fixed in Version

Frama-C Oxygen-20120901

Summary

0000251: 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).

Tags

No tags attached.

Attached Files

imprecise.c [^] (325 bytes) 2009-09-20 19:29 [Show Content] [Hide Content]

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;
}

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