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が、いくつかの単純化はすでに行われているかもしれません。これらの内部単純化をオフにできるとは思いません。