Wie prüft Klee, ob der Test bestanden wurde oder nicht?

Question

Ich habe das Klee-Tutorial unter Klee tutorial gelesen. Es ist ziemlich einfach und geradlinig. Wenn ich jedoch Dateien überprüfe, die durch den Test unter KLEE generated files erzeugt wurden, habe ich keine Datei gefunden, die mir sagt, ob der Test bestanden oder nicht bestanden wurde. Es gibt zwei Möglichkeiten, die Testergebnisse zu überprüfen.

1. KLEE ist intelligent genug, um zu wissen, was der erwartete Rückgabewert der 3 Testfälle

2. KLEE einfach den Rückgabewert irgendwo in einer Datei Dump und den menschlichen Entwickler brauchen, um sie selbst zu überprüfen.

Ist das so?

Answer 1

Klee gibt Ihnen nicht die Ausgabe Ihres Programms, das auf den Tests läuft, weil es Ihren Code statisch (meistens) analysiert. Es läuft also nicht wirklich und deshalb ist es schnell. Wenn es Ihr Programm ausführen wollte, würde es viel mehr Zeit benötigen. Sie müssen es nur selbst ausführen und sehen, ob die Ausgabe Ihren Erwartungen entspricht oder nicht.

Klee ist ein Testeingabe-Generierungstool, kein Testfall-Generierungstool. Der Unterschied besteht darin, dass ein Testfall sowohl eine Eingabe als auch eine erwartete Ausgabe hat.

Answer 2

KLEE verwendet LLVM Testing Infrastructure llvm-lit für Komponententests. Der Befehl und die Bestanden/Nicht bestanden-Prüfung werden in Kommentare geschrieben.

Nehmen Sie zum Beispiel test/Feature/DoubleFree.c.

// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc 
// RUN: rm -rf %t.klee-out 
// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s 
// RUN: test -f %t.klee-out/test000001.ptr.err 

int main() { 
    int *x = malloc(4); 
    free(x); 
    // CHECK: memory error: invalid pointer: free 
    free(x); 
    return 0; 
}