不支持ACSL结构的Eva插件Frama-C

Question

我目前正试图用Frama和它的插件 Eva来评估一个测试套件。为此，我使用以下标志运行Frama：

frama-c -eva -cpp-extra-args="-DINCLUDEMAIN -I .../<headerfile folder>" <some c file>.c

Frama (24.0)是通过Opam安装的.当运行eva时，一个输出是：

[eva] using spcification for function strcpy

和

[eva] FRAMAC_SHARE/libc/string.h:373:cannot evaluate ACSL term, unsupported ACSL construct: logic function strcmp

如您所见：Eva状态不支持ACSL构造。

在查看string.h .h (~/.opam/default/share/frama-c/libc)文件时，我找到了strcpy函数：

/*@
...
@ ensures equal_contents: strcmp(dest,src) == 0;
@ ensures result_ptr: \result == dest;
@*/
extern char *strcpy(char *restrict dest, const char *restrict src);

而strcmp函数：

/*@ requires valid_string_s1: valid_read_string(s1);
                       `@ requires valid_string_s2: valid_read_string(s2);
@ assigns \result \from indirect:s1[0..], indirect:s2[0..];
              @ ensures acsl_c_equiv: \result == strcmp(s1,s2);
 @*/
extern int strcmp (const char *s1, const char *s2);

据我所知，Eva在ACSL合同中使用这个文件来知道确切需要检查哪些内容，并且给出了strcmp的ACSL合同。

有人知道为什么会出现这个错误信息吗?如何解决这个问题？

非常感谢！

Answer 1

Eva不支持所有ACSL结构。值得注意的是，strcmp是由一个公理(参见__fc_string_axiomatics.h)定义的，它对WP插件很好，但对Eva非常不利。有几件事你可以做：

• 决定你不在乎。如果strcmp的结果不精确这一事实对您的分析并不重要，那么Eva不能评估这种后状态并不重要。
• 在解析的文件列表中包括来自Frama的string.c的libc：这将提供strcmp的定义，Eva将对其进行分析。注意，由于这个定义基本上是您所期望的for循环，如果您想要一个精确的结果，您可能需要调整Eva的精确选项。基本上，只需在命令行中添加$(frama-c -print-share-path)/libc/string.c即可。
• 提供您自己的函数定义。