时间戳

首页 > 解决方案 > 满足 memcpy 的证明义务？[Frama-C]

frama-c - 满足 memcpy 的证明义务？[Frama-C]

问题描述

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

出现的障碍之一与满足wp插件在遇到memcpy调用时生成的证明义务有关。具体而言，以下三项义务： memcpy_proof_obligations

从“目标”注释来看，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 understand WP memory models

标签： frama-c

解决方案

正如您在评论中提到的那样，正确的解决方案是使用-wp-model "Typed+Cast"以便让 WP 接受强制转换void*（更准确地说，它会考虑到这一点，p并且(void*)p对于任何指针来说都是一样的，这足以证明requiresof memcpy）。现在，正如您链接到的问题的答案中所述，此内存模型的主要问题（以及它不是默认值的原因）是它本质上是不安全的：它依赖于根据定义无法评估的假设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;
}

基本上，默认的内存模型确保了andTyped所指向的位置（即 的后置条件）之间的分离，因为and是不同的，您既不能证明 的后置条件，也不能将其用作推导in的假设，因为模型中根本无法表达平等。cxfintcharg\falsemain

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

推荐阅读