加载 .C 文件时 Frama-C 报告 "invalid ghost in extern linkage specification"

Question

我是 Frama-C 的新手，所以我可能遗漏了一些明显的东西。当我尝试加载我的项目文件（其中有一些 .C 文件）时，Frama-C 在控制台中报告以下错误 window 并停止处理

  [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 函数规范库中，也许吧？我是运行 Frama-C 20.0（钙）Ubuntu 19.10。 Frama-C 是通过 opam 安装的。深入了解这意味着什么将非常有用。

Answer 1

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

带有血腥技术细节的更长答案： 如果您在名为 file.C（后缀为大写 C）的文件上启动 frama-c（没有非常实验性的 frama-clang plug-in），预处理器调用Frama-C 将认为它正在处理 C++ 源文件。从技术上讲，这意味着它将定义标准 _cplusplus 宏，这反过来意味着 Frama-C 的 libc 的 stdlib.h 文件中的 __BEGIN_DECL 宏将被扩展就像包含在 C++ 中一样（即 extern "C" {）。

如果安装了 frama-clang，它会负责解析文件，并且应该会成功。如果不是这种情况，将调用正常的 Frama-C 解析器。它对处理 extern "C" 链接规范有一些有限的支持，因为它们可以在某些共享 C/C++ headers 中随意出现，尽管严格来说这不是标准 C，但不是所有构造都在此上下文中处理。

加载 .C 文件时 Frama-C 报告 "invalid ghost in extern linkage specification"

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

frama-c