frama-c - 满足 memcpy 的证明义务吗？ [框架-C]

Question

我们一直在使用 Frama-C 对商业项目进行“实验性”静态分析(集成到我们的 CI 中，在整个代码库的一小部分上进行一些选择性阻塞检查) .

出现的问题之一涉及满足 wp 插件在遇到 memcpy 调用时生成的证明义务。具体而言，以下三项义务:

从“目标”注释来看，Frama-C 似乎正在尝试证明目标内存和源内存是有效的。

我尝试添加 requires\valid() 先决条件，但这似乎没有帮助。在这些情况下，被测函数内的 memcpy 调用会将数据从输入参数复制到函数，并将该数据放入局部变量(作用域在函数内)。

更复杂的是，复制数据的局部变量是打包结构中的一个属性。

具体来说，我希望有人能够分享一些 memcpy 使用的真实示例，可以满足 wp 引入的目标(例如，什么先决条件)我必须添加才能证明它吗？)

如果重要的话，我正在运行 Frama-C Magnesium-20151002(根据 Ubuntu 16 上的 apt-get，这是“最新的”)，并使用以下参数进行调用:


frama-c -wp -wp-split -wp-dynamic -lib-entry -wp-proof alt-ergo -wp-report


也相关，但缺少一个清晰的工作示例:Frama-c : Trouble understanding WP memory models

Answer 1

正如您在评论中提到的，正确的解决方案是使用 -wp-model "Typed+Cast"为了让 WP 接受来自 void* 的强制转换(更准确地说，它会认为 p 和 (void*)p 对于任何指针来说都是相同的，这足以证明 requires 的 memcpy )。现在，正如 the answer 中提到的对于您链接到的问题，此内存模型的主要问题(以及它不是默认模型的原因)是它本质上不安全:它依赖于根据定义无法评估的假设WP本身。这是一个突出这个问题的小例子:

int x;
char* c;

/*@ assigns c;
    ensures c == ((char *)&x);
*/
void g(void) {
  c = &x;
}

/*@ assigns \nothing;
    ensures \separated(&x,c);
*/
void f() {
}

void main () {
g();
f();
//@ assert \false;
}

基本上，默认Typed内存模型确保 c 指向的位置之间的分离和x (即 f 的后置条件)，因为 int和char是不同的，你都无法证明 g 的后置条件或者用它作为假设来推导\false在main ，因为等式根本无法在模型中表达。

现在，如果您使用 Typed+Cast ， g 的后置条件现在已经被正确理解了，而且证明起来也很简单。 WP 不会让你同时证明&x和c分开，因为他们一起参与一项任务。然而，在 f不存在这样的赋值，并且后置条件也很容易证明，导致证明 \false在main因为我们对 &x 有两个相互矛盾的陈述和c 。更一般地说，WP 依赖本地别名分析来跟踪不同类型指针之间的潜在别名(全局分析将违背模块化分析器的目的)。传递选项-wp-model +Cast因此可以被视为告诉 WP“相信我，程序不会创建错误输入的别名”的方式。然而，可以手动传递别名信息(或者借助尚未编写的全局别名检测插件)。例如，使用选项 -wp-alias-vars x,c f 的后置条件变成Unknown (即 &x 和 c 之间的分离不再是一个假设，即使对于 f 也是如此)。