Slicing für mehrere Assert

Question

Ist es möglich, Frama-C Slicing-Plugin zu verwenden, um für mehr als eine Behauptung Slice?

z. Geben Sie den folgenden Code:

#include "assert.h" 

int main() { 
    double a=3; 
    double b=4; 
    b=a+b; 
    double c=123; 

//@ assert(b>=0); 

    double d=a/b; 
    c=a; 

//@ assert(c==0); 

    if (a<b) 
     a=c; 

    return 0; 
} 

Ich möchte die Scheibe für beide Assertions erhalten.

Answer 1

Option -slice-assert main wählt als Slicing-Kriterium alle Aussagen der Funktion main. In der Tat können Sie nicht direkt auswählen, in Bezug auf nur eine von ihnen zu schneiden. Sie müssen auf //@ slice pragma expr b; für die erste oder //@ slice pragma expr c; für die zweite zurückgreifen.

Allgemeiner gesagt, sind Slicing-Kriterien kumulativ: Je mehr Kriterien Sie angeben, desto mehr Code wird beibehalten.