0001536: Binding of label in annotations is strange

View Issue Details [ Jump to Notes ]

[ 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

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

Relationships

Notes

~0004552

2014-02-12 16:57

Fix committed to stable/neon branch.

Notes

Date Modified	Username	Field	Change
Issue History
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
2013-10-29 15:45	svn	Status	confirmed => resolved
2013-10-29 15:45	svn	Resolution	open => fixed
2013-12-19 01:11		Source_changeset_attached	=> framac master e09bdaed
2014-02-12 16:53		Source_changeset_attached	=> framac stable/neon e09bdaed
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

Issue History