Frama-C \strlen 函数答案

【问题标题】：Frama-C \strlen functionFrama-C \strlen 函数
【发布时间】：2015-08-04 18:25:55
【问题描述】：

我安装了 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 选项）无效。

【问题讨论】：

不应该是char *strcpy()吗？该函数返回您为*dest 传递的指针。
@Olaf: \strlen 在此上下文中用于检查 src 是否指向有效的 C 字符串。是的，它返回一个字符 *。错字已修复。
所以不是同名的C函数？使用同一个名字很烦人。
了解 \strlen 如何检查有效的 C 字符串会很有趣，它的唯一参数是指针。
@WeatherVane 在 ACSL 中的逻辑函数不需要是可计算的。如果您放弃此要求，则很容易使用 \forall 量化指针参数后的所有字符来编写 \strlen 的定义。

标签： c string strlen frama-c

【解决方案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] != '\0')
  @       && s[i] == '\0') ==> strlen(s) == i;
  @
  @ axiom strlen_neg{L}:
  @   \forall char* s;
  @      (\forall ℤ i; 0 <= i ==> s[i] != '\0')
  @      ==> strlen(s) < 0;

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

您可能还对文档ACSL by example 感兴趣，该文档指定并证明了一些常用功能。

【讨论】：