frama-c - 我想在 Frama-C 中生成所有先决条件，主要是初始先决条件

Question

我想根据 calculus.ml 代码生成由 Frama-C 生成的所有先决条件，这些先决条件存储在一个表中。我主要有兴趣获得转换为逻辑公式并发送给求解器的初始谓词。这可以做到吗？请帮我打印发送给求解器的初始谓词。我正在尝试的代码如下：

int main()  
{  
    int x=42,y=40;  
    if(x<50)  
    {  
        x=x+2; y=x-y;  
    }   
    else  
    {  
        x=x-2; y=x-y;  
    }  
    //@ assert P: y>0;  
}

Answer 1

我认为你可以通过使用该-wp-out dir选项得到你想要的，然后在目录中查看生成.ergo的文件dir，但可能已经做了一些简化。我认为您不能关闭这些内部简化。