关于WP将依赖未证后置条件的RTE断言标记为surely valid的问询

1. 这些断言是否应标记为valid under hypotheses？ #

是的，这些断言理应被标记为valid under hypotheses。

根据WP插件的定义：

• surely valid 属性是完全无需依赖任何未被证明的假设（包括未验证的函数契约）就能成立的；
• valid under hypotheses 属性则是依赖了未证的前置/后置条件（比如search函数未证明的ensures契约，或是foo调用search时未被保证的前置要求）才能成立的。

你遇到的情况里，rte_2、rte_3、rte_4的成立完全依赖于两个未证假设：

• search函数的后置条件确实成立；
• foo调用search时满足了search的前置要求（但foo本身没有前置条件约束输入，比如main传NULL的场景就会违反）。

WP默认把未证的函数契约当作假设来使用，且默认的-report没有区分这种依赖关系，才会错误地把这类属性标成surely valid。

2. 轻量区分方法 #

有几个轻量的方式可以实现区分，最直接的是调整Frama-C的命令行选项：

• 使用-wp-report-hyp选项：
  在命令中加入该选项，WP会在报告里显式标记出依赖未证假设的属性，不会再和真正的surely valid混淆。完整命令示例：

  frama-c search.c -wp -wp-report-hyp -then -report
  

  这个选项会让依赖未证契约/假设的属性在报告中被明确标注为依赖假设的有效，而非surely valid。

• 查看详细证明日志：
  加入-wp-verbose（或简写-wp-v）选项，WP会输出每个属性的证明过程细节，其中会明确列出该属性依赖的所有假设，包括未证的函数契约。示例命令：

  frama-c search.c -wp -wp-v -then -report
  

  你可以从日志里快速判断哪些属性是依赖未证条件的。

• 启用-report -show-hypotheses：
  当使用-report时，加上-show-hypotheses参数，报告会列出每个属性依赖的所有假设，包括未被验证的部分，帮助你区分真正的surely valid和依赖假设的属性。

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