berechnet Erreichbarkeit zu einer Funktion ist frama-c die Wertanalyse

Question

Hier mein Beispiel:

int in; 
int sum(int n){ 
    int log_input = n; 
    int log_global = in; 
    return 0; 
} 

int main(){ 
    int n = Frama_C_interval(-10, 10); 
    in = n; 
    if (n > 0){ 
     sum(n + 4); 
    } 
    return 0; 
} 

Was ich möchte, ist zu tun, um den Bereich der Eingangsgröße n zu finden, wenn sie in Haupt initialisiert, dass die Ergebnisse in Erreichen der Funktionssumme. Der korrekte Bereich in diesem Beispiel ist [1, 10].

In der Probe, würde Ich mag den ursprünglichen Eingang in einem globalen Wert in und wieder einführen sie in der Funktion Summe zu „retten“, indem sie in die Variable log_global zuweisen und damit den ursprünglichen Eingang zu entdecken, die in Folge beim Erreichen der Funktion. Wenn wir frama-c in diesem Beispiel ausführen, erhalten wir, dass der Bereich von log_input [5, 14] und der Bereich von log_global [-10, 10] ist. Ich verstehe, warum das passiert - der Wert in wird am Anfang von Haupt festgelegt und wird nicht durch weitere Manipulationen an n beeinflusst.

Ich fragte mich, ob es eine einfache Möglichkeit gibt, dies in frama-c zu ändern? Vielleicht eine einfache Modifikation in frama-cs Code?

Eine unabhängige Idee, die ich hatte, war die if-Anweisung in Haupt zu manipulieren:

if (in > 0){ 
    sum(in + 4); 
} 

ich verwenden, um die globale Variable statt n. Dies führt zwar zu dem richtigen Bereich, aber diese Lösung skaliert nicht gut zu komplizierteren Funktionen und tieferen Aufrufstapeln.

Answer 1

Hier ist eine mögliche Lösung. Verwenden Sie das eingebaute Frama_C_interval_split und ein entsprechendes -slevel N (hier, mindestens N=21). Die Funktion sum wird N-mal untersucht werden, ein für jeden möglichen Wert von N, und das Ergebnis wird

int n = Frama_C_interval_split(-10, 10); 

Die Ergebnisse genau sein:

[value] Values at end of function sum: 
    log_input ∈ [5..14] 
    log_global ∈ [1..10] 
    __retres ∈ {0} 

(Im Prinzip entspricht dies das Durchführen manuelle Profis- Überprüfung, so dass die Leistungen für große Werte von N nicht gut sein werden.)