frama-c - "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 契约(Contract)可以构建为一系列行为，这些行为描述了可能调用该函数的各种情况(有关更多信息，请参见 ACSL manual)。它们是这样介绍的:

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

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

所谓的默认行为包含了不属于显式行为的条款:有点像你写的契约(Contract)是这样的:

/*@
  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 的输出中，这让事情变得更加困惑。

更新 正如一位受人尊敬的前同事所建议的，我对 from 子句缺少报告进行了一些研究:默认情况下，未尝试的属性不会显示-report，你必须显式设置-report-untried(然后给你所有你不调用的标准库函数的先决条件，以及from of get_len 如预期)。