Frama-C Bug Tracking System - Frama-C
View Issue Details
0000672Frama-CKernelpublic2011-01-17 14:552012-09-19 17:16
Assigned Tovirgile 
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 files.tgz (374) 2011-01-17 14:55

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
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:41svn
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