|
Notes |
|
|
|
|
(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. |
|
|
|
|
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). |
|
|
|
|
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! |
|
|
|
|
|
Remark 0002409 dealt with by introducing a function loc_to_locs, more precise than loc_to_loc. |
|
|
|
|
|
Fix committed to stable/neon branch. |
|