编译 E-ACSL FRAMA-C 时出错
Error compiling E-ACSL FRAMA-C
我是 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 and the flags the 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”标签,因为它 returns 另一个错误。
Frama-C最新版本:Sulfur-20171101
知道发生了什么吗?
谢谢!
通常,您应该在与 frama-c
二进制文件相同的目录中安装一个名为 e-acsl-gcc.sh
的脚本,它可以使用适当的选项调用 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
Edit 查看脚本使用的链接命令,我会说手册中较早提出的命令行已过时(特别是,它指的是eacsl-jemalloc
而 e-acsl-gcc.sh
似乎更喜欢 eacsl-dlmalloc
),这可能被报告为 https://bts.frama-c.com
处的错误
我是 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 and the flags the 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”标签,因为它 returns 另一个错误。
Frama-C最新版本:Sulfur-20171101 知道发生了什么吗?
谢谢!
通常,您应该在与 frama-c
二进制文件相同的目录中安装一个名为 e-acsl-gcc.sh
的脚本,它可以使用适当的选项调用 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
Edit 查看脚本使用的链接命令,我会说手册中较早提出的命令行已过时(特别是,它指的是eacsl-jemalloc
而 e-acsl-gcc.sh
似乎更喜欢 eacsl-dlmalloc
),这可能被报告为 https://bts.frama-c.com