Bedeutung von \ alt in ACSL Nachbedingungen

Question

Ich bin ein Neuling Benutzer von Frama-C und habe ein paar Fragen zu Aussagen über Zeiger.

Betrachten Sie das C-Fragment unter Einbeziehung:

• zwei verwandte Datenstrukturen Daten und Griff, S. T. Handle hat einen Zeiger auf Data;
• ein Feld 'state' in Daten, die angeben, ob eine hypothetische Operation abgeschlossen wurde
• drei Funktionen: init(), start_operation() und wait();
• a main() Funktion, um die oben verwendet wird, und mit 6 Assertions (A1-A6)

Nun, warum es ist, daß A5 und A6 können nicht mit dem WP Verifizierer ("frama-c -WP geltend gemacht werden, file.c ") Sollten sie wegen der letzten" Gewähren "-Klausel auf start_operation() nicht halten?

Was mache ich falsch?

Best,

Eduardo

typedef enum 
{ 
    PENDING, NOT_PENDING 
} DataState; 

typedef struct 
{ 
    DataState state; 
    int value; 
} Data; 


typedef struct 
{ 
    Data* data; 
    int id; 
} Handle; 

/*@ 
    @ ensures \valid(\result); 
    @ ensures \result->state == NOT_PENDING; 
    @*/ 
Data* init(void); 

/*@ 
    @ requires data->state == NOT_PENDING; 
    @ ensures data->state == PENDING; 
    @ ensures \result->data == data; 
    @*/ 
Handle* start_operation(Data* data, int to); 

/*@ 
    @ requires handle->data->state == PENDING; 
    @ ensures handle->data->state == NOT_PENDING; 
    @ ensures handle->data == \old(handle)->data; 
    @*/ 
void wait(Handle* handle); 


int main(int argc, char** argv) 
{ 
    Data* data = init(); 
    /*@ assert A1: data->state == NOT_PENDING; */ 

    Handle* h = start_operation(data,0); 
    /*@ assert A2: data->state == PENDING; */ 
    /*@ assert A3: h->data == data; */ 

    wait(h); 
    /*@ assert A4: h->data->state == NOT_PENDING; */ 
    /*@ assert A5: data->state == NOT_PENDING; */ 
    /*@ assert A6: h->data == data; */ 

    return 0; 
} 

Answer 1

Wenn Sie einen „Neuling“ knifflige Speicher Manipulationen zu überprüfen.

Das ACSL-Konstrukt \old funktioniert nicht genau so, wie Sie es denken.

Zuerst \old(handle) in einem post-Zustand ist die gleiche wie handle, weil handle ein Parameter ist. Ein Vertrag soll aus Sicht der Anrufer verwendet werden. Selbst wenn die Funktion wait modifiziert handle (was ungewöhnlich wäre, aber möglich ist), wäre ihr Vertrag immer noch dazu gedacht, die vom Argument als Argument übergebenen Werte und den von der Funktion an den Aufrufer zurückgegebenen Zustand in Beziehung zu setzen.

Kurz gesagt, in einem ACSL Post Zustand, parameter bedeutet immer \old(parameter) (auch wenn die Funktion parameter wie eine lokale Variable modifiziert).

Zweitens ist die obige Regel nur für Parameter. Bei globalen Variablen und Speicherzugriffen wird davon ausgegangen, dass die Nachbedingung für den Poststatus gilt, wie Sie es von seinem Namen erwarten würden. Das Konstrukt \old(handle)->data, das Sie geschrieben haben, und das entspricht handle->data, bedeutet "das Feld .data, dass der alte Wert von Handle in den neuen Zustand zeigt", so dass die Nachbedingung handle->data == \old(handle)->data eine Tautologie ist und wahrscheinlich nicht das, was Sie beabsichtigten.

Aus dem Kontext scheint es, dass Sie handle->data == \old(handle->data) stattdessen bestimmt, was bedeutet, „das Feld .data, dass der alte Wert von handle Punkten im Neuzustand auf das Feld gleich .data, dass der alte Wert von handle Punkten in der alter Zustand ". Mit dieser Änderung werden alle Behauptungen in Ihrem Programm für mich bewiesen (unter Verwendung von Alt-Ergo 0.93).