"Default behavior: tried with Frama-C kernel." 是什么意思？

Question

我正在尝试验证来自 Frama-C + WP 的简单程序。

#include <string.h>

/*@
        requires valid_read_string(s);
        assigns \result \from indirect:s[0..];
        ensures \result == strlen(s);
*/
size_t get_len(const char *s) {
        return strlen(s);
}

int main() {
        static const char foo[4] = { 'H', 'e', 'y', 0 };
        size_t sz = get_len(foo);
        //@ assert sz == 3;

        return 0;
}

除一个证明外，一切都正确验证：

frama-c -rte -pp-annot -wp -wp-rte /tmp/test.c -c11 -then -report -report-no-proven

[    -    ] Default behavior
            tried with Frama-C kernel.

     1 To be validated
     1 Total

我似乎找不到任何关于此“默认行为”的含义的信息，也无法弄清楚为什么无法验证它。

我是不是做错了什么？

Answer 1

ACSL 合同可以构建为行为列表，这些行为描述了可能调用函数的各种情况（有关详细信息，请参阅 ACSL manual）。它们是这样介绍的：

/*@ 
  behavior A:
    assumes some_condition;
    requires ...
    assigns ...
    ensures ...
  behavior B: ...
*/

如果调用函数时assumes子句为真，则行为激活，必须满足行为中的其他子句

所谓的默认行为包含了不属于显式行为的条款：有点像你的合同是这样写的：

/*@
  behavior Default:
    assumes \true;
    requires valid_read_string(s);
    assigns \result \from indirect:s[0..];
    ensures \result == strlen(s);
*/

行为的有效性状态（包括默认行为）只是其组件状态的合并（即当且仅当所有组件都通过验证时它才有效）。它由内核根据插件（此处为 WP）放置在每个单独组件上的状态计算得出。

现在，“未知”从何而来，因为看起来所有注释都已被证明？事实上，情况并非如此：您编写 assigns 子句的方式 assigns \result \from indirect:s[0..]; 暗示有两件事需要证明：首先，该函数不会修改程序的全局状态（这是由WP），其次，结果只取决于 s 的内容（这还没有做到，事实上目前还没有插件能够做到这一点）。这是第二个属性，通常称为 from 子句，它导致内核认为默认行为未得到充分证明。不幸的是，这个 from 子句似乎甚至没有出现在 Report 的输出中，这让事情变得更加混乱。

UPDATE 正如一位受人尊敬的前同事所建议的那样，我深入研究了 from 子句缺少报告的情况：默认情况下，未尝试的属性不存在-report显示，你必须显式设置-report-untried（然后给你所有你不调用的标准库函数的前提条件，以及[=的from 20=] 符合预期）。

Answer 2

Virgile 的回答非常好（FD：我们是前同事），但我想指出的是，在你非常严格的情况下，你可以证明 from你的合同条款。更确切地说，一旦它被纠正，你就可以证明它。正确的子句是

        assigns \result \from direct:s[0..], indirect:s

确实需要读取s指向的字符串的内容来计算其长度，并且间接依赖指针s来访问要读取的内存. （direct/indirect 依赖项的概念不是 ACSL 的一部分，添加它是为了使 from 子句对使用 Eva 插件的程序的验证更有用。）

更精确的版本是

        assigns \result \from direct:s[0..StrLen(s)], indirect:s

但是如果 s 并且它指向的内存不准确，这就更难证明了。

最后，能够执行证明的插件是插件From，启用了选项-from-verify-assigns。注意证明不是WP做的，是Eva+From做的。特别是，证明不是模块化的。相反，检查合约以查找从 main 开始的执行期间发生的 get_len 的所有调用点。这可能是也可能不是您要找的。

"Default behavior: tried with Frama-C kernel." 是什么意思？

What does "Default behavior: tried with Frama-C kernel." mean?

frama-c