编译 E-ACSL FRAMA-C 时出错答案

【问题标题】：Error compiling E-ACSL FRAMA-C编译 E-ACSL FRAMA-C 时出错
【发布时间】：2018-04-03 17:31:22
【问题描述】：

我是 Frama-C 框架的新手，我正在尝试使用 C 程序进行一些合同测试。我打算为此使用 E-ACSL 插件，我尝试了一个测试程序来查看它是如何工作的，但是我得到了一些编译错误。这是我的代码：

#include <stdio.h>
#include <stdlib.h>

int main(void) {
int x = 0;
  /*@ assert x == 1;*/
  /*@ assert x == 0;*/
  return 0;
}

那么，这里是 Frama-C 注释的代码：

/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
struct __e_acsl_mpz_struct {
   int _mp_alloc ;
   int _mp_size ;
   unsigned long *_mp_d ;
};
typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
/*@ ghost extern int __e_acsl_init; */

/*@ ghost extern int __e_acsl_internal_heap; */

extern size_t __e_acsl_heap_allocation_size;

/*@
predicate diffSize{L1, L2}(ℤ i) =
  \at(__e_acsl_heap_allocation_size,L1) -
  \at(__e_acsl_heap_allocation_size,L2) ≡ i;

*/
int main(void)
{
  int __retres;
  int x = 0;
  /*@ assert x ≡ 1; */ ;
  /*@ assert x ≡ 0; */ ;
  __retres = 0;
  return __retres;
}

最后，我尝试使用 gcc 和 manual 指示的标志（第 13 页）编译它，但我收到以下错误（和警告）：

$ gcc monitored_second.c -o monitored_second -leacsl -leacsl-gmp -leacsl -jemalloc -lpthread -lm

monitored_second.c:10:1: warning: ‘__FC_BUILTIN__’ attribute directive ignored [-Wattributes]
 typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];

monitored_second.c:18:55: warning: ‘__FC_BUILTIN__’ attribute directive ignored [-Wattributes]
                                                   int line);
                                                   ^
monitored_second.c:25:60: warning: ‘__FC_BUILTIN__’ attribute directive ignored [-Wattributes]
                                                        size_t ptr_size);
                                                        ^
/usr/bin/ld: cannot find -leacsl
/usr/bin/ld: cannot find -leacsl-jemalloc
collect2: error: ld returned 1 exit status

我还删除了“-rtl-bittree”标签，因为它返回另一个错误。

Frama-C 版本是最新的：Sulfur-20171101 知道发生了什么吗？

谢谢！

【问题讨论】：

警告在第 13 页解释。
我认为您可能需要传递一个-L 链接器标志，告诉编译器在哪里可以找到您要链接的库。查找包含名为 libeacsl.so 或类似文件的目录。

标签： gcc frama-c acsl

【解决方案1】：

通常，您应该将一个名为e-acsl-gcc.sh 的脚本安装在与frama-c 二进制文件相同的目录中，它可以使用适当的选项来处理调用gcc。它的基本用法记录在手册的第 2.2 节中，man e-acsl-gcc.sh 提供了有关可以使用的选项的更多详细信息。简而言之，您应该可以输入

e-acsl-gcc.sh -c \
  --oexec-eacsl=first_monitored \
  --oexec=first \
  --ocode=first_monitored.i \
  first.i

获得

带有 e-acsl 工具的可执行文件 first_monitored
带有原始程序的可执行文件first
带有 e-acsl 生成的 C 代码的源文件 first_monitored.i

编辑查看脚本使用的链接命令，我会说手册中前面提出的命令行已过时（特别是，它指的是eacsl-jemalloc，而@ 987654331@ 似乎更喜欢eacsl-dlmalloc)，这可能会在https://bts.frama-c.com 上报告为错误

【讨论】：