时间戳

首页 > 解决方案 > 如何在 Frama-C 中调用关于 libc 字符串函数的公理？

frama-c - 如何在 Frama-C 中调用关于 libc 字符串函数的公理？

问题描述

__fc_string_axiomatic.hFrama-C 在头文件中为来自 C 标准库的字符串函数提供公理化规范。例如，一个这样的条目指定memset()读取：

/*@ axiomatic MemSet {
  @ logic  memset{L}(char *s, ℤ c, ℤ n)
  @   reads s[0..n - 1];
  @ // Returns [true] iff array [s] contains only character [c]
  @
  @ axiom memset_def{L}:
  @   \forall char *s; \forall ℤ c; \forall ℤ n;
  @      memset(s,c,n) <==> \forall ℤ i; 0 <= i < n ==> s[i] == c;
  @ }
  @*/

在我自己的带注释的 C 文件中，我尝试利用以下公理规范memset()：

int n = strlen(argv[1]);
//@ assert n >= 0;
char dest[n+1];
//@ assert \valid(dest+ (0..n));
//@ assert \valid(argv[1]+ (0..n));


memset(dest,0,n+1);
//@ assert \forall integer k; 0 <= k < n+1 ==> dest[k] == 0;

尽管最后的断言似乎是谓词 in 的替代品memset_def，而且 Frama-C 确实评估了axiomatic上面显示的内容，但 Alt-Ergo 未能证明这一断言。我对验证 C 标准库本身不感兴趣；我的问题是：如何强制 Frama-C 在我自己的断言中调用该公理？

标签： frama-cformal-verification

解决方案

您的断言立即被 Z3 4.4.1 证明，但实际上不是 Alt-Ergo。因此，问题在于 Alt-Ergo 用于解决目标的策略，而不是 Frama-C 生成的内容。一种可能性是添加触发器来帮助 Alt-Ergo，但我不清楚我们可以将它们放在哪里。

推荐阅读