1

我目前正在尝试使用 Frama-C评估一个测试套件，它是插件Eva。为此，我使用以下标志运行 Frama-C：

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

Frama-C (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 states unsupported ACSL construction。

在查看 string.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.

有人知道为什么会出现此错误消息以及如何解决此问题吗？
非常感谢提前！！！

4

1 回答 1

1

Eva 不支持所有 ACSL 结构。值得注意的是，strcmp它是由一个公理定义的（请参阅 参考资料__fc_string_axiomatics.h），这对 WP 插件有好处，但对 Eva 很不利。您可以做几件事：

  • 决定你不在乎。如果结果不精确这一事实strcmp对您的分析并不重要，那么 Eva 无法评估此后置条件并不重要。
  • 在您解析的文件列表中包含string.c来自 Frama-C 的文件：这将提供Eva 将分析的定义。请注意，由于此定义基本上是您所期望的循环，因此如果您想要一个精确的结果，您可能需要调整 Eva 的精度选项。基本上，为此，只需在命令行中添加即可。libcstrcmpfor$(frama-c -print-share-path)/libc/string.c
  • 提供您自己的函数定义。
于 2022-02-11T16:57:41.640 回答