I would like to generate all the preconditions mainly initial preconditions in Frama-C

Question

I would like to generate all the preconditions generated by Frama-C which are stored in a table according to the calculus.ml code. I am mainly interested to get the initial predicate which is converted to logic formula and sent to the solvers. Can this be done? Please help me to print the initial predicate which is sent to the solvers. The code I am trying with is given below:

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

I think that you can get what you wish by using the -wp-out dir option, and then look at the generated .ergo file in the dir directory, but some simplifications might already have been done. I don't think that you can turn off these internal simplifications.