Frama-C Bug Tracking System - Frama-C
View Issue Details
0001480Frama-CKernel > ACSL implementationpublic2013-09-17 13:572014-03-13 15:57
Assigned Toyakobowski 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001480: assigns \result \from ...; in the AST should be pretty-printed as any other assigns clause
Descriptionint 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).
TagsNo tags attached.
Attached Files

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
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...
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 :-)
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)
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 ?
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.

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:11svn
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