Frama-C Bug Tracking System - Frama-C | |||||
View Issue Details | |||||
ID | Project | Category | View Status | Date Submitted | Last Update |
0002507 | Frama-C | Kernel | public | 2020-06-06 23:39 | 2020-10-06 10:00 |
Reporter | dgenin | ||||
---|---|---|---|---|---|
Assigned To | AllanBlanchard | ||||
Priority | normal | Severity | major | Reproducibility | have not tried |
Status | closed | Resolution | no change required | ||
Platform | x86 | OS | Ubuntu | OS Version | 19.10 |
Product Version | Frama-C 20-Calcium | ||||
Target Version | Fixed in Version | ||||
Summary | 0002507: Frama-C reports “invalid ghost in extern linkage specification” while loading files | ||||
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 | ||||
Tags | No tags attached. | ||||
Relationships | |||||
Attached Files |
Notes | |||||
|
|||||
|
|
||||
|
|||||
|
|
Issue History | |||||
Date Modified | Username | Field | Change | ||
---|---|---|---|---|---|
2020-06-06 23:39 | dgenin | New Issue | |||
2020-06-09 17:13 | dgenin | Note Added: 0006978 | |||
2020-10-06 10:00 | AllanBlanchard | Note Added: 0006980 | |||
2020-10-06 10:00 | AllanBlanchard | Status | new => closed | ||
2020-10-06 10:00 | AllanBlanchard | Assigned To | => AllanBlanchard | ||
2020-10-06 10:00 | AllanBlanchard | Resolution | open => no change required |