SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:issue:440 [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:issue:440

back to the bts

The current fix is to avoid creation of blocks at parsing time to separate annotations and labels. Old behavior was to treat

/*@ assert \true; */
L: ;

as

/*@ assert \true; */
{ L: ; }

New behavior does not add block. Due to the current AST representation, this also means that L: and the assert are attached to the same statement (while the assert was considered to be before L: in the previous setting). This is closer to what the ACSL manual says, but can lead to changes in some particular cases, especially for the annotations of the slicing plugin:

/*@ slice pragma stmt; */
L: ;

has a slightly different scope: in the previous behavior, the statement of interest was a block containing a labelled statement, while it is now directly the labelled statement. in particular, in

if (foo) goto L;
/*@ slice pragma stmt; */
L: ;

the old behavior would preserve if(foo) goto L; in the slice (we jump directly in the block), while this is not the case anymore (we always go to the next statement, the goto is in fact a no-op).

mantis/frama-c/issue/440.txt · Last modified: 2010/06/02 11:16 by virgile