Frama-C reports "invalid ghost in extern linkage specification" while loading .C files

Question

I am very new to Frama-C so perhaps I'm missing something obvious. As I try to load my project files (with some .C files among them) 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

It seems like the error is in Frama-C function spec library, maybe? I'm running Frama-C 20.0 (Calcium) on Ubuntu 19.10. Frama-C was installed via opam. Any insight into what this means would be very useful.

Answer 1

tl; dr: don't use .C instead of .c as a suffix for a C file. In particular gcc recognizes by default that suffix as C++ instead of C source.

longer answer with gory technical details: If you launch frama-c (without the very experimental frama-clang plug-in) on a file named file.C (with an uppercase C as suffix), the preprocessor called by Frama-C will consider that it is handling a C++ source file. Technically, this means that it will define the standard _cplusplus macro, which in turn implies that the __BEGIN_DECL macro found in the stdlib.h file of Frama-C's libc will be expanded as if included in a C++ (i.e. as extern "C" {).

Had frama-clang been installed, it would have taken care of parsing the file, and should have succeeded. When this is not the case, the normal Frama-C parser is called. It has some limited support for handling extern "C" linkage specifications, as they can appear in the wild in some shared C/C++ headers, even though strictly speaking this is not standard C, but not all constructions are handled in this context.