Frama-C Bug Tracking System - Frama-C
View Issue Details
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
Steps To Reproduce
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.
Relationships
Attached Filestgz files.tgz (374) 2011-01-17 14:55
https://bts.frama-c.com/file_download.php?file_id=151&type=bug
Issue History
Date ModifiedUsernameFieldChange
2011-01-17 14:55yakobowskiNew Issue
2011-01-17 14:55yakobowskiFile Added: files.tgz
2011-01-17 15:10signolesStatusnew => assigned
2011-01-17 15:10signolesAssigned To => virgile
2011-10-19 16:01virgileNote Added: 0002400
2011-10-19 16:01virgileStatusassigned => acknowledged
2011-10-20 14:41svnCheckin
2011-10-20 14:41svnStatusacknowledged => resolved
2011-10-20 14:41svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

Notes
(0002400)
virgile   
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.