在加载.C文件时，Frama-C报告 "外部链接规范中的无效鬼魂"。

Question

我对Frama-C非常陌生，所以也许我错过了一些明显的东西。当我试图加载我的项目文件（其中包括一些.C文件）时，Frama-C在控制台窗口中报告了以下错误并停止处理

  [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

好像是Frama-C函数规范库出了问题，可能是？我在Ubuntu 19.10上运行Frama-C 20.0（钙）。Frama-C是通过以下方式安装的 opam. 任何关于这意味着什么的见解都将是非常有用的。

Answer 1

tl; dr: 不要使用 .C 而不是 .c 作为C文件的后缀。特别是 gcc 默认情况下识别该后缀为C++而非C源码。

较长的回答，有血淋淋的技术细节。如果你启动 frama-c (没有非常实验性的 frama-clang 插件）的文件上，名为 file.C (带大写 C 作为后缀），Frama-C调用的预处理器将认为它正在处理一个C++源文件。技术上，这意味着它将定义标准的 _cplusplus 宏，这又意味着 __BEGIN_DECL 中的宏 stdlib.h Frama-C的libc文件将被展开，就像包含在C++中一样（即以 extern "C" {).

如果安装了frama-clang，它就会对文件进行解析，并且应该会成功。如果不是这样，就会调用普通的Frama-C解析器。它有一些有限的支持来处理 extern "C" 链接规范，因为它们可以在一些共享的CC++头文件中出现在野外，尽管严格来说这不是标准的C，但并不是所有的构造都会在这种情况下处理。