Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0002507Frama-CKernelpublic2020-06-06 23:392020-10-06 10:00
Reporterdgenin 
Assigned ToAllanBlanchard 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionno change required 
Platformx86OSUbuntuOS Version19.10
Product VersionFrama-C 20-Calcium 
Target VersionFixed in Version 
Summary0002507: Frama-C reports “invalid ghost in extern linkage specification” while loading files
DescriptionAs I try to load my project files Frama-C reports the following error in the Console window and stops processing [kernel] FRAMAC_SHARE/libc/__fc_alloc_axiomatic.h:30: invalid ghost in extern linkage specification: Location: between lines 30 and 45, before or at token: } 28 #include "__fc_define_wchar_t.h" 29 30 __BEGIN_DECLS 31 32 /*@ ghost extern int __fc_heap_status __attribute__((FRAMA_C_MODEL)); */ 33 34 /*@ axiomatic dynamic_allocation { 35 @ predicate is_allocable{L}(integer n) // Can a block of n bytes be allocated? 36 @ reads __fc_heap_status; 37 @ // The logic label L is not used, but it must be present because the 38 @ // predicate depends on the memory state 39 @ axiom never_allocable{L}: 40 @ \forall integer i; 41 @ i < 0 || i > __FC_SIZE_MAX ==> !is_allocable(i); 42 @ } 43 */ 44 45 __END_DECLS 46 47 __POP_FC_STDLIB
Steps To Reproducenot sure
Additional Information
TagsNo tags attached.
Relationships
Attached Files
Issue History
Date ModifiedUsernameFieldChange
2020-06-06 23:39dgeninNew Issue
2020-06-09 17:13dgeninNote Added: 0006978
2020-10-06 10:00AllanBlanchardNote Added: 0006980
2020-10-06 10:00AllanBlanchardStatusnew => closed
2020-10-06 10:00AllanBlanchardAssigned To => AllanBlanchard
2020-10-06 10:00AllanBlanchardResolutionopen => no change required

Notes
(0006978)
dgenin   
2020-06-09 17:13   
I traced the issue to the case of the file extension. It seems that if the file extension is .C the file is interpreted as C++ (maybe) and including stdlib.h causes the fault. I haven't checked if other librareris cause an issue. If the extension is .c then the file is interpreted as plain C and the file loads normally.
(0006980)
AllanBlanchard   
2020-10-06 10:00   
This indeed due to the fact that the `.C` is seen as a C++ file. Note that for C++, an experimental Front-end is available: Frama-Clang.