时间戳

首页 > 解决方案 > 为什么 while 循环基于条件表达式的类型检查（w/tc_expr）？

verifiable-c - 为什么 while 循环基于条件表达式的类型检查（w/tc_expr）？

问题描述

似乎这tc_expr仅限于对类型上下文的了解，因此无法安全地“类型检查”需要了解堆状态的表达式，例如作为 while 循环条件的指针取消引用。为什么会这样，我是否有可能证明正确的循环，例如：

char *t = ...;
...
while (*t != 0)
{
    ...
    t++;
}

我认为 while 循环可以有选择地通过一种变体来证明tc_expr，它允许通过考虑堆上下文和键入上下文来取消引用指针。我怀疑这种想法是循环条件应该是一个“纯”表达式，但我最终很好奇这是否真的是一个必要的约束。

PS我意识到我可以将其重写为for循环。我的问题仍然存在，知道 VST 允许我证明这种循环，尽管语法不同。

标签： verifiable-c

解决方案

答案 1： 这是一个设计决策，无论哪种方式，我们发现如果表达式不访问内存，许多事情会更简单（并且更符合分离逻辑的精神）。

答案 2： 您可以按原样编写此 while 循环。然后将 clightgen 与-normalize标志一起使用（无论如何你都应该使用它），然后你可以验证它。但是，在这种情况下，循环形式（严格来说）不是 Clight“while”循环，而是if (?) then /*skip*/; else break;在循环体的中间有它的循环测试（）；所以你将用forward_loop它来证明它，而不是forward_while.

推荐阅读