ID0002507: **This issue was created automatically from Mantis Issue 2507. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002507 | Frama-C | Kernel | public | 2020-06-06 | 2020-10-06 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | dgenin | **Assigned To** | AllanBlanchard | **Resolution** | no change required | | **Priority** | normal | **Severity** | major | **Reproducibility** | have not tried | | **Platform** | x86 | **OS** | Ubuntu | **OS Version** | 19.10 | | **Product Version** | Frama-C 20-Calcium | **Target Version** | - | **Fixed in Version** | - | ### Description : As 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 Reproduce : not sure