2021-03-05 08:32 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000993Frama-CPlug-in > frompublic2014-02-12 16:59
Reporteryakobowski 
Assigned Toyakobowski 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0002405

yakobowski (manager)

(This is actually a pdg problem, but there is no "pdg" category.)

~0002406

Anne (reporter)

Very strange indeed ! I try to find why...

~0002407

Anne (reporter)

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)

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)

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)

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)

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)

Remark 0002409 dealt with by introducing a function loc_to_locs, more precise than loc_to_loc.

~0004717

yakobowski (manager)

Fix committed to stable/neon branch.
+Notes

-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
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
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
2013-12-19 01:12 yakobowski Source_changeset_attached => framac master 7c66a1c6
2013-12-19 01:12 pascal Source_changeset_attached => framac master e0ae5c82
2014-02-12 16:54 yakobowski Source_changeset_attached => framac stable/neon 7c66a1c6
2014-02-12 16:54 pascal Source_changeset_attached => framac stable/neon e0ae5c82
2014-02-12 16:59 yakobowski Note Added: 0004717
2014-02-12 16:59 yakobowski Status closed => resolved
+Issue History