Frama-C在加载.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（Calcium）。 Frama-C是通过opam安装的。对这意味着什么的任何见解将非常有用。

Answer 1

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

更长距离的回答，带有血腥的技术细节：如果在名为frama-c的文件（后缀为大写frama-clang）上启动frama-clang（没有非常试验性的file.C插件），则Frama-C调用的预处理器将认为它正在处理C ++源文件。从技术上讲，这意味着它将定义标准的C宏，这又意味着在Frama-C的libc的_cplusplus文件中找到的__BEGIN_DECL宏将被扩展，就好像包含在C ++中一样（即[ C0]）。

如果已安装frama-clang，它将负责解析文件，并且应该成功。如果不是这种情况，则会调用普通的Frama-C解析器。它对处理stdlib.h链接规范提供了一些有限的支持，因为它们可能会在某些共享的C / C ++头文件中出现在野外，即使严格地说这不是标准C，但并非所有构造都在此上下文中处理。