Frama-C \strlen 函数

Question

我安装了 Frama-C Sodium (20150201) + Jessie 插件，我正在尝试重现 ACSL 参考手册中提供的示例。但是我不能使用 Jessie 库函数（比如 \strlen），因为每次我使用其中一个时，我都会得到如下错误：

[kernel] user error: unbound function \strlen in annotation.

这是代码：

/*@
      requires \base_addr(src) != \base_addr(dest);
      requires \strlen(src) >= 0;
*/
char *strcpy ( char * dest , const char * src );

从 bash 启动 frama-c（使用 -jessie 选项）无效。

Answer 1

Frama-C 实现目前不支持逻辑函数 \strlen。如果你下载ACSL 1.9 (Sodium implementation) 手册，你会看到定义是红色的，意思是不支持。

相反，您可以尝试用函数 strlen 替换 \strlen，其公理定义在您的 Frama-C 安装文件 libc/__fc_string_axiomatic.h 中给出。为此，请确保在示例的开头添加 #include <string.h>。（string.h 自动包含 __fc_string_axiomatic.h）

我在定义 strlen:

的公理块 StrLen 的开头下方重现

  @ axiomatic StrLen {
  @ logic ℤ strlen{L}(char *s);
  @ // reads s[0..];
  @
  @ axiom strlen_pos_or_null{L}:
  @   \forall char* s; \forall ℤ i;
  @      (0 <= i
  @       && (\forall ℤ j; 0 <= j < i ==> s[j] != '[=10=]')
  @       && s[i] == '[=10=]') ==> strlen(s) == i;
  @
  @ axiom strlen_neg{L}:
  @   \forall char* s;
  @      (\forall ℤ i; 0 <= i ==> s[i] != '[=10=]')
  @      ==> strlen(s) < 0;

文件 __fc_string_axiomatic.h 的大部分定义最初是为 Jessie 编写的，因此您应该能够证明 strcpy 的规范——如果您提供足够强大的循环不变量.

您可能还对说明和证明一些常用函数的文档 ACSL by example 感兴趣。

Frama-C \strlen 函数

Frama-C \strlen function

c

string

strlen

frama-c