Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000672Frama-CKernelpublic2011-01-17 14:552012-09-19 17:16
Reporteryakobowski 
Assigned Tovirgile 
PrioritynormalSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20101202-beta2 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0000672: Incorrect cil merging in presence of ACSL annotations
DescriptionLaunching Frama-C on the three attached files with the -check option causes a crash with the error
builtin.h:6:[kernel] failure: [AST Integrity Check]
            initial ASTlogic variable Frama_C_entropy_source(728) is not declared
Additional InformationCommand-line:
    frama-c builtin.h builtin.c main.c -check

Three different files seem to be needed. The error also depends on the order the files are passed on the command line.
TagsNo tags attached.
Attached Filestgz file icon files.tgz [^] (374 bytes) 2011-01-17 14:55

- Relationships

-  Notes
(0002400)
virgile (developer)
2011-10-19 16:01

- Only two files are necessary (builtin.h and main.c)
- There are at least two issues: the presence of a prototype for Frama_C_nondet in main.c will trigger a different check issue than without.

- Issue History
Date Modified Username Field Change
2011-01-17 14:55 yakobowski New Issue
2011-01-17 14:55 yakobowski File Added: files.tgz
2011-01-17 15:10 signoles Status new => assigned
2011-01-17 15:10 signoles Assigned To => virgile
2011-10-19 16:01 virgile Note Added: 0002400
2011-10-19 16:01 virgile Status assigned => acknowledged
2011-10-20 14:41 svn Checkin
2011-10-20 14:41 svn Status acknowledged => resolved
2011-10-20 14:41 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker