Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001536Frama-CKernel > ACSL implementationpublic2013-10-28 16:012014-03-13 15:57
Reporterbobot 
Assigned Tovirgile 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001536: Binding of label in annotations is strange
DescriptionThe 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.
TagsNo 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker