Frama-C: No splitting of if-statement
<p>I have the following problem when analyzing if-conditions with my plugin. When I analyze code like</p>

<pre><code>if ((a &amp;&amp; b) || c)
</code></pre>

<p>Frama-C creates code like this:</p>

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

<p>For my analysis, I want to get the control-flow without the conditions split up, so that one statement remains. I want this, because by splitting up the conditional, the reaching of _LOR is dependent on the or-part only.</p>

<p><em>Example</em>: creating the CFG as in the <code>viewcfg</code> plugin of the developer guide leads to this:</p>

<p><a href="https://i.stack.imgur.com/4fySN.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/4fySN.png" alt="CFG"></a></p>

<p><code>a=(a+b)+c</code> can be reached in the <code>then</code> and the <code>else</code>-path of <code>if a</code>, which I cancel out in my plugin in the block-statement (so that after a "simple" <code>if</code>, the statement is not dependent on the condition anymore).</p>

<p>Is there a possibility to block the splitting of the <code>if</code>, by a command-line argument or something like that?</p>