Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001480Frama-CKernel > ACSL implementationpublic2013-09-17 13:572014-03-13 15:57
Reportercorrenson 
Assigned Toyakobowski 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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

- Relationships

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


- 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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker