Frama-C reports “invalid ghost in extern linkage specification” while loading files
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