如何在Frama-C及WP插件中断言程序中的不可达代码点？

在Frama-C的WP插件中，直接使用//@ assert \unreachable;这个ACSL注解就能断言目标代码点不可达，完全符合你期望的效果。

使用示例如下：

// 假设x的取值范围恒非负
if (x < 0) {
    //@ assert \unreachable;
    puts("此代码行永远不会被执行");
}

WP插件分析时会验证该断言：若验证通过，说明该代码点确实无执行路径可达；若验证失败，会生成反例指出存在可达该位置的执行场景。

\unreachable是Frama-C ACSL规范中的内置谓词，专门用于标记不可达代码位置，WP插件原生支持对该断言的验证。

内容的提问来源于stack exchange，提问作者Costava