0001480: assigns \result \from ...; in the AST should be pretty-printed as any other assigns clause

(0004074)
correnson (manager)
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 (developer)
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 (manager)
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 (developer)
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 (manager)
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 (manager)
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.

Issue History
Date Modified	Username	Field	Change
2013-09-17 13:57	correnson	New Issue
2013-09-17 13:57	correnson	Status	new => assigned
2013-09-17 13:57	correnson	Assigned To	=> virgile
2013-09-17 14:08	correnson	Note Added: 0004074
2013-09-17 14:15	virgile	Note Added: 0004075
2013-09-17 14:15	virgile	Summary	assigns \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:45	yakobowski	Assigned To	virgile => yakobowski
2013-09-17 22:48	yakobowski	Note Added: 0004080
2013-09-18 09:10	virgile	Note Added: 0004082
2013-09-18 12:32	correnson	Note Added: 0004083
2013-11-22 21:55	yakobowski	Note Added: 0004334
2013-11-22 22:11	svn	Checkin
2013-11-22 22:38	yakobowski	Note Edited: 0004334
2013-12-07 18:52	yakobowski	Status	assigned => resolved
2013-12-07 18:52	yakobowski	Resolution	open => fixed
2014-03-13 15:56	signoles	Fixed in Version	=> Frama-C Neon-20140301
2014-03-13 15:57	signoles	Status	resolved => closed

Notes
(0004074) correnson (manager) 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 (developer) 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 (manager) 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 (developer) 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 (manager) 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 (manager) 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.

Relationships