Search code examples
frama-c

Frama-C: No splitting of if-statement

I have the following problem when analyzing if-conditions with my plugin. When I analyze code like

if ((a && b) || c)

Frama-C creates code like this:

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

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.

Example: creating the CFG as in the viewcfg plugin of the developer guide leads to this:

CFG

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

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

Solution

  • An undocumented and unsupported solution exists. Before compiling Frama-C, in function initCIL of cil.ml, change

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

    into

    theMachine.useLogicalOperators <- true;

    The normalization will use logical || and && operators instead of gotos.

    Please note that this is unsupported for a good reason. The Frama-C plugins packaged with the kernel expect an AST in which those operators are not used, so they will probably crash or do something unsound on your program. Use at your own risk!