|
Notes |
|
|
|
Autre cas intéressant à voir avec la GUI :
/*@
assigns \result ;
assigns \result \from x ;
*/
int f(int x) { return ++x; }
/*@
assigns \result ;
assigns \result \from \nothing ;
ensures \result == 4 ;
*/
int g(void) { return f(3); }
# frama-c -wp -val -main g |
|
|
|
|
|
If we do not display the assigns \result; line but only assigns \result from foo;, there no place where to put the bullet corresponding to the assigns property... |
|
|
|
|
After discussion with Virgile, the change must be done inside the pretty-printer. Every thing else is already ok.
Possible choice:
I) for assigns \result \from ..., do we display
I.1) assigns \result
I.2) assigns \nothing
(which means we are going to print
assigns \nothing
assigns \result \from ... )
II) for assigns \result \from ..., x \from ..., do we display
II.1) assigns \result, x
II.2) assigns x
Please vote :-) |
|
|
|
|
For I), there is no alternative, we must display assigns \result; Mixing
assigns \nothing; and assigns \result \from foo; is not a valid ACSL spec.
For II), I tend to prefer II.2) |
|
|
|
|
I) as said Virgile, the parser complains when mixing result and nothing
II) Also prefer II.2)
This a mexican vote, doesn't it ? |
|
|
|
(0004334)
|
|
yakobowski
|
2013-11-22 21:55
(Last edited: 2013-11-22 22:38) |
|
Mixing I.1) and II.2) is really too ugly, because of the asymmetry on the presence of \result in the non-from clause. I cannot implement this in good conscience :-)
If you really want II.2), I propose we relax the requirements that forbid I.2. Commit for I.1 + II.1 is forthcoming.
|
|