Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000993Frama-CPlug-in > frompublic2011-10-20 21:302014-02-12 16:59
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000993: Incorrect dependencies in presence of declared functions
DescriptionConsider the following code

//@ assigns *p \from \nothing;
void f(int *p);

void main () {
  int x = 0;
  int y = 0;

  f(&x);
  f(&y);
}

Slicing the program on x results on keeping only y and the call f(&y), instead of the instructions related to x. (However, the result is correct with -calldeps.)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0002405)
yakobowski (manager)
2011-10-21 00:20

(This is actually a pdg problem, but there is no "pdg" category.)
(0002406)
Anne (reporter)
2011-10-21 09:07

Very strange indeed ! I try to find why...
(0002407)
Anne (reporter)
2011-10-21 09:17

It seems that it is a [from] problem :
$ frama-c -deps toto.c

[from] Function f:
[from] x FROM \nothing
[from] y FROM \nothing

I think that before, there were an information about [default: true] meaning that [x] might not be modified by [x] but it seems that it disappeared ?

I'll change the category to have Pascal explanations...
(0002409)
pascal (reporter)
2011-10-21 10:09

Must do a better job depending whether the location is inexact because of evaluation approximations or because of Tset in the destination part of the assigns clause.
(0002413)
yakobowski (manager)
2011-10-22 13:52

Independently of remark 2409, which will be dealt with in a near future, I think we left a bug.

pdg.c:
//@ assigns *p \from \nothing;
void f(int *p);

void main (int m) {
  int x = 0;
  f(&x);
}

frama-c -slice-value x -slice-print pdg.c

The result is
void main(void)
{
  int x;
  f(& x);
  return;
}

However, according to the semantics of acsl assigns, it is incorrect to remove the initializer for x, as f might not write in x. The problem still lies within the froms:
[from] Function f:
         x FROM \nothing

Since the assigns are never certain, I think we should always add "(and SELF)" in the results to be correct. Alternatively, we can campaign for adding a "strong assigns" keyword to ACSL :-)
(0002414)
pascal (reporter)
2011-10-22 14:19

The assigns are never certain, but the dependencies are certain. It is only possible that no assignment occurs if the target variable itself is part of the dependencies. x CANNOT not depend on x at the end of the function and be untouched at the same time.

"strong" assigns already mean something else that would be useful (the function doesn't touch any variable not in its strong assigns at any point of its execution).
(0002415)
yakobowski (manager)
2011-10-22 14:34

My bad, my understanding of dependencies was apparently faulty, and "It is only possible that no assignment occurs if the target variable itself is part of the dependencies" was not clear to me.

Concerning the second point, I should have proposed "sure assigns" instead of "strong assigns". But given the current semantics, my point is moot anyway, as we can already express anything needed. Great!
(0002449)
yakobowski (manager)
2011-11-04 00:11

Remark 0002409 dealt with by introducing a function loc_to_locs, more precise than loc_to_loc.
(0004717)
yakobowski (manager)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-10-20 21:30 yakobowski New Issue
2011-10-20 21:30 yakobowski Status new => assigned
2011-10-20 21:30 yakobowski Assigned To => Anne
2011-10-21 00:20 yakobowski Note Added: 0002405
2011-10-21 09:07 Anne Note Added: 0002406
2011-10-21 09:17 Anne Note Added: 0002407
2011-10-21 09:18 Anne Category Plug-in > slicing => Plug-in > functional dependencies
2011-10-21 09:18 Anne Assigned To Anne => pascal
2011-10-21 10:07 svn Checkin
2011-10-21 10:09 pascal Note Added: 0002409
2011-10-22 13:52 yakobowski Note Added: 0002413
2011-10-22 14:19 pascal Note Added: 0002414
2011-10-22 14:34 yakobowski Note Added: 0002415
2011-10-23 21:45 yakobowski Assigned To pascal => yakobowski
2011-11-04 00:11 yakobowski Note Added: 0002449
2011-11-04 00:18 svn Checkin
2011-11-04 00:18 svn Status assigned => resolved
2011-11-04 00:18 svn Resolution open => fixed
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:59 yakobowski Note Added: 0004717
2014-02-12 16:59 yakobowski Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker