2021-03-01 23:04 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001480Frama-CKernel > ACSL implementationpublic2014-03-13 15:57
Assigned Toyakobowski 
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




correnson (manager)

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


virgile (developer)

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...


yakobowski (manager)

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


virgile (developer)

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)


correnson (manager)

I) as said Virgile, the parser complains when mixing result and nothing
II) Also prefer II.2)
This a mexican vote, doesn't it ?


yakobowski (manager)

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
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
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
+Issue History