Frama-C: Aucune division de l'instruction if

Question

Je rencontre le problème suivant lors de l'analyse des conditions if avec mon plugin. Lorsque j'analyse du code comme

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

Frama-C crée du code comme ceci :

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

Pour mon analyse, je veux obtenir le flux de contrôle sans que les conditions soient séparées, de manière à ce qu'une seule instruction reste. Je veux cela, car en séparant la condition, l'atteinte de _LOR dépend uniquement de la partie `ou`.

Exemple : créer le CFG comme dans le plugin viewcfg du guide du développeur mène à ceci :

a=(a+b)+c peut être atteint dans le chemin du then et du else de if a, ce que je supprime dans mon plugin dans le bloc d'instructions (afin qu'après un `if` "simple", l'instruction ne dépende plus de la condition).

Existe-t-il une possibilité de bloquer la séparation du if, par un argument en ligne de commande ou quelque chose du genre ?

Answer 1

Une solution non documentée et non pris en charge existe. Avant de compiler Frama-C, dans la fonction initCIL de cil.ml, modifiez

theMachine.useLogicalOperators <- false (* ne pas utiliser les opérateurs LAND et LOR paresseux *);

en

theMachine.useLogicalOperators <- true;

La normalisation utilisera les opérateurs logiques || et && au lieu des goto.

Veuillez noter que ceci n'est pas pris en charge pour une bonne raison. Les plugins Frama-C fournis avec le noyau s'attendent à un AST dans lequel ces opérateurs ne sont pas utilisés, ils risquent donc probablement de planter ou de produire un résultat incorrect sur votre programme. Utilisez à vos propres risques !