如何断言一个点不可达？答案

【问题标题】：How to assert that a point is unreachable?如何断言一个点不可达？
【发布时间】：2022-09-28 05:42:51
【问题描述】：

对于 Frama-C 和 WP 插件，用户如何断言程序中的某个点不可达？

寻找类似的东西：

//@ assert \\unreachable;

标签： c frama-c acsl

【解决方案1】：

您可以使用//@ assert \false; 断言某个点不可达，因为：

一个（可证明的）不可到达的断言总是被证明是真的

通过Introduction to C program proof with Frama-C and its WP plugin 艾伦布兰查德。

例如对于给定文件main.c：
/*@
  assigns \nothing;
*/
int foo(const int input) {
    int result = 0;

    if (input > 0) {
        result += 1;

        if (input < 0) {
            // This assertion will be proved successfully
            // because this location is provably unreachable.
            //@ assert \false;

            result += 1;
        }
    }

    return result;
}
验证断言是否被证明：
$ frama-c -wp main.c
[kernel] Parsing main.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] Proved goals:    3 / 3
  Qed:             3
以上使用的是frama-c 25.0 版（锰）。

【讨论】：