Frama-C：不拆分 if 语句答案

【问题标题】：Frama-C: No splitting of if-statementFrama-C：不拆分 if 语句
【发布时间】：2016-06-03 08:20:56
【问题描述】：

在使用我的插件分析 if 条件时，我遇到了以下问题。当我分析像

这样的代码时

if ((a && b) || c)

Frama-C 创建如下代码：

if (a) {
    if (b){
        goto _LOR;
    }
    else{
        goto _LAND;
    }
}
else{
    _LAND: ;
    if (c) {
        _LOR: //....

对于我的分析，我希望在不拆分条件的情况下获得控制流，以便保留一条语句。我想要这个，因为通过拆分条件，_LOR 的到达仅取决于 or 部分。

示例：在开发者指南的viewcfg 插件中创建CFG 会导致：

a=(a+b)+c 可以在then 和else 路径中到达if a，我在我的插件中的块语句中将其取消（这样在“简单”if 之后，该语句不再依赖于条件）。

是否有可能通过命令行参数或类似的方式阻止 if 的拆分？

【问题讨论】：

作为一种解决方法，您可以观察到该语句依赖于if c（因为它仅在其一个分支中），而if c 依赖于if b 和if a。因此可以得出结论，该语句取决于三个条件。
@Anne 当然是完全正确的：_LOR 和 a 和 b 之间存在间接依赖关系，通过传递性。其实这种依赖已经被Frama-C的From插件处理了。
@byako 是的，将所有依赖项向下推是完全有意义的，看看上面的例子，它完全可以工作（我会得到a&&b or !a&&c or a&&!b&&c。但问题是，我想要语句所依赖的最少条件。（并连接）。因此，我必须在有 2 个或更多路径合并的块处取消它。例如，在具有单个条件的 if-else-trees 中。与@Anne 的方式，我会得到完整的依赖关系，不知道什么/什么时候取消。我希望我的意思很清楚，否则我可以添加一个例子。
使用 or's，我将不得不对所有可能的 if 组合进行交叉乘积，这在较大的程序中可能非常庞大。由于您的回答似乎对我有用，我会做一些进一步的测试，看看使用不受支持的版本是否会导致任何问题。

标签： frama-c

【解决方案1】：

存在未记录和不受支持的解决方案。在编译Frama-C之前，在cil.ml的函数initCIL中，改变

theMachine.useLogicalOperators <- false (* do not use lazy LAND and LOR *);

进入

theMachine.useLogicalOperators <- true;

规范化将使用逻辑 || 和 && 运算符而不是 goto。

请注意，这是有充分理由的。与内核一起打包的 Frama-C 插件需要一个不使用这些运算符的 AST，因此它们可能会崩溃或对您的程序做一些不正确的事情。使用风险自负！

【讨论】：