Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #56
Closed
Open
Issue created Jun 06, 2020 by mantis-gitlab-migration@mantis-gitlab-migration

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking