Frama-C Bug Tracking System - Frama-C
View Issue Details
0001480Frama-CKernel > ACSL implementationpublic2013-09-17 13:572014-03-13 15:57
correnson 
yakobowski 
normalminoralways
closedfixed 
 
Frama-C Neon-20140301 
0001480: assigns \result \from ...; in the AST should be pretty-printed as any other assigns clause
int x,y; //@ assigns x \from y ; void f (void); //@ assigns \result \from y ; int g (void); Pour f : la clause "assigns x" est visible dans l'AST. Pour g : il manque la clause "assigns \nothing" dans l'AST (qui est pourtant prouvée par le WP).
No tags attached.
Issue History
2013-09-17 13:57corrensonNew Issue
2013-09-17 13:57corrensonStatusnew => assigned
2013-09-17 13:57corrensonAssigned To => virgile
2013-09-17 14:08corrensonNote Added: 0004074
2013-09-17 14:15virgileNote Added: 0004075
2013-09-17 14:15virgileSummaryassigns \result \from ... assigns \nothing, doesn't it ? => assigns \result \from ...; in the AST should be pretty-printed as any other assigns clause
2013-09-17 22:45yakobowskiAssigned Tovirgile => yakobowski
2013-09-17 22:48yakobowskiNote Added: 0004080
2013-09-18 09:10virgileNote Added: 0004082
2013-09-18 12:32corrensonNote Added: 0004083
2013-11-22 21:55yakobowskiNote Added: 0004334
2013-11-22 22:11svnCheckin
2013-11-22 22:38yakobowskiNote Edited: 0004334
2013-12-07 18:52yakobowskiStatusassigned => resolved
2013-12-07 18:52yakobowskiResolutionopen => fixed
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004074)
correnson   
2013-09-17 14:08   
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
(0004075)
virgile   
2013-09-17 14:15   
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...
(0004080)
yakobowski   
2013-09-17 22:48   
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 :-)
(0004082)
virgile   
2013-09-18 09:10   
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)
(0004083)
correnson   
2013-09-18 12:32   
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   
(edited on: 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.