Frama-C：不拆分 if 语句

Question

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

这样的代码时

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，我在块语句中的插件中取消了（所以在 "simple" if 之后，语句不再依赖于条件。

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

Answer 1

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

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

进入

theMachine.useLogicalOperators <- true;

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

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

Frama-C: No splitting of if-statement