Frama-C Bug Tracking System - Frama-C
View Issue Details
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

Notes
(0002405)
yakobowski   
2011-10-21 00:20   
(This is actually a pdg problem, but there is no "pdg" category.)
(0002406)
Anne   
2011-10-21 09:07   
Very strange indeed ! I try to find why...
(0002407)
Anne   
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   
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   
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   
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   
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   
2011-11-04 00:11   
Remark 0002409 dealt with by introducing a function loc_to_locs, more precise than loc_to_loc.
(0004717)
yakobowski   
2014-02-12 16:59   
Fix committed to stable/neon branch.

Issue History
2011-10-20 21:30yakobowskiNew Issue
2011-10-20 21:30yakobowskiStatusnew => assigned
2011-10-20 21:30yakobowskiAssigned To => Anne
2011-10-21 00:20yakobowskiNote Added: 0002405
2011-10-21 09:07AnneNote Added: 0002406
2011-10-21 09:17AnneNote Added: 0002407
2011-10-21 09:18AnneCategoryPlug-in > slicing => Plug-in > functional dependencies
2011-10-21 09:18AnneAssigned ToAnne => pascal
2011-10-21 10:07svn
2011-10-21 10:09pascalNote Added: 0002409
2011-10-22 13:52yakobowskiNote Added: 0002413
2011-10-22 14:19pascalNote Added: 0002414
2011-10-22 14:34yakobowskiNote Added: 0002415
2011-10-23 21:45yakobowskiAssigned Topascal => yakobowski
2011-11-04 00:11yakobowskiNote Added: 0002449
2011-11-04 00:18svn
2011-11-04 00:18svnStatusassigned => resolved
2011-11-04 00:18svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2013-12-19 01:12yakobowskiSource_changeset_attached => framac master 7c66a1c6
2013-12-19 01:12pascalSource_changeset_attached => framac master e0ae5c82
2014-02-12 16:54yakobowskiSource_changeset_attached => framac stable/neon 7c66a1c6
2014-02-12 16:54pascalSource_changeset_attached => framac stable/neon e0ae5c82
2014-02-12 16:59yakobowskiNote Added: 0004717
2014-02-12 16:59yakobowskiStatusclosed => resolved