0001536: Binding of label in annotations is strange

View Issue Details [ Jump to Notes ] [ Related Changesets ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0001536

Frama-C

Kernel > ACSL implementation

public

2013-10-28 16:01

2014-03-13 15:57

Reporter

bobot

Assigned To

virgile

Priority

normal

Severity

major

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Fluorine-20130601

Target Version

Fixed in Version

Frama-C Neon-20140301

Summary

0001536: Binding of label in annotations is strange

Description

The following function without "LLoop:" type-check, with it doesn't.

======================
void f() {
  int i;
LInit:

  {
  LLoop:
    i = 0;
    //@ assert \at(1,LInit) == 1;
  }
}
======================

[kernel] preprocessing with "gcc -C -E -I. error_typer.c"
error_typer.c:8:[kernel] user error: logic label `LInit' not found in annotation.
[kernel] user error: skipping file "error_typer.c" that has errors.
[kernel] Frama-C aborted: invalid user input.

Tags

No tags attached.

Attached Files

Relationships

Notes
(0004552) 2014-02-12 16:57	Fix committed to stable/neon branch.

Issue History
Date Modified	Username	Field	Change
2013-10-28 16:01	bobot	New Issue
2013-10-28 16:01	bobot	Status	new => assigned
2013-10-28 16:01	bobot	Assigned To	=> virgile
2013-10-28 16:52	virgile	Status	assigned => confirmed
2013-10-29 15:45	svn	Checkin
2013-10-29 15:45	svn	Status	confirmed => resolved
2013-10-29 15:45	svn	Resolution	open => fixed
2014-02-12 16:57		Note Added: 0004552
2014-03-13 15:56	signoles	Fixed in Version	=> Frama-C Neon-20140301
2014-03-13 15:57	signoles	Status	resolved => closed