diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/Feature/KleeExecTreeBogus.test | 50 | ||||
| -rw-r--r-- | test/Feature/WriteExecutionTree.c | 18 | ||||
| -rw-r--r-- | test/lit.cfg | 2 |
4 files changed, 36 insertions, 36 deletions
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index ae038b80..a7d748c6 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -147,7 +147,7 @@ file(GENERATE add_custom_target(systemtests COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}" - DEPENDS klee kleaver klee-ptree klee-replay kleeRuntest ktest-gen ktest-randgen + DEPENDS klee kleaver klee-exec-tree klee-replay kleeRuntest ktest-gen ktest-randgen COMMENT "Running system tests" USES_TERMINAL ) diff --git a/test/Feature/KleeExecTreeBogus.test b/test/Feature/KleeExecTreeBogus.test index 11fe87c8..5926d128 100644 --- a/test/Feature/KleeExecTreeBogus.test +++ b/test/Feature/KleeExecTreeBogus.test @@ -1,65 +1,65 @@ REQUIRES: sqlite3 fail on broken db (not sqlite) -RUN: not %klee-ptree tree-info %S/ptree-dbs/not_a.db 2> %t.err +RUN: not %klee-exec-tree tree-info %S/exec-tree-dbs/not_a.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-CORRUPT -input-file=%t.err %s -CHECK-CORRUPT: Can't prepare read statement: file is not a database +CHECK-CORRUPT: Cannot prepare read statement: file is not a database empty tree RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/empty_db.csv nodes" -RUN: %klee-ptree tree-info %t.db > %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/empty_db.csv nodes" +RUN: %klee-exec-tree tree-info %t.db > %t.err RUN: FileCheck -check-prefix=CHECK-EMPTY -input-file=%t.err %s CHECK-EMPTY: Empty tree. fail on tree with duplicate node IDs RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/duplicated_node.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/duplicated_node.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-DUP -input-file=%t.err %s -CHECK-DUP: PTree DB contains duplicate child reference or circular structure. Affected node: 2 +CHECK-DUP: ExecutionTree DB contains duplicate child reference or circular structure. Affected node: 2 fail on invalid branch type RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_btype.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/invalid_btype.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-BTYPE -input-file=%t.err %s -CHECK-BTYPE: PTree DB contains unknown branch type (123) in node 1 +CHECK-BTYPE: ExecutionTree DB contains unknown branch type (123) in node 1 fail on invalid termination type RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/invalid_ttype.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/invalid_ttype.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-TTYPE -input-file=%t.err %s -CHECK-TTYPE: PTree DB contains unknown termination type (123) in node 3 +CHECK-TTYPE: ExecutionTree DB contains unknown termination type (123) in node 3 fail on tree with looping nodes RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/loop.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/loop.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-LOOP -input-file=%t.err %s -CHECK-LOOP: PTree DB contains duplicate child reference or circular structure. Affected node: 1 +CHECK-LOOP: ExecutionTree DB contains duplicate child reference or circular structure. Affected node: 1 fail on tree with missing node (child node ID > max. ID) RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_after_max.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/missing_after_max.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-MISSA -input-file=%t.err %s -CHECK-MISSA: PTree DB contains references to non-existing nodes (> max. ID) in node 3 +CHECK-MISSA: ExecutionTree DB contains references to non-existing nodes (> max. ID) in node 3 fail on tree with missing node (child node ID < max. ID) RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/missing_before_max.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/missing_before_max.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-MISSB -input-file=%t.err %s -CHECK-MISSB: PTree DB references undefined node. Affected node: 4 +CHECK-MISSB: ExecutionTree DB references undefined node. Affected node: 4 fail on illegal node ID (0) RUN: rm -f %t.db -RUN: %sqlite3 -separator ',' %t.db ".import %S/ptree-dbs/node_id0.csv nodes" -RUN: not %klee-ptree tree-info %t.db 2> %t.err +RUN: %sqlite3 -separator ',' %t.db ".import %S/exec-tree-dbs/node_id0.csv nodes" +RUN: not %klee-exec-tree tree-info %t.db 2> %t.err RUN: FileCheck -check-prefix=CHECK-ID0 -input-file=%t.err %s -CHECK-ID0: PTree DB contains illegal node ID (0) +CHECK-ID0: ExecutionTree DB contains illegal node ID (0) cleanup RUN rm -f %t.db diff --git a/test/Feature/WriteExecutionTree.c b/test/Feature/WriteExecutionTree.c index e7bf59ce..42f531a5 100644 --- a/test/Feature/WriteExecutionTree.c +++ b/test/Feature/WriteExecutionTree.c @@ -1,13 +1,13 @@ // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee -write-ptree --output-dir=%t.klee-out %t.bc -// RUN: %klee-ptree branches %t.klee-out/ptree.db | FileCheck --check-prefix=CHECK-BRANCH %s -// RUN: %klee-ptree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s -// RUN: %klee-ptree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s -// RUN: %klee-ptree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s -// RUN: %klee-ptree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s -// RUN: %klee-ptree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s -// RUN: not %klee-ptree dot %t.klee-out/ptree-doesnotexist.db +// RUN: %klee -write-exec-tree --output-dir=%t.klee-out %t.bc +// RUN: %klee-exec-tree branches %t.klee-out/exec_tree.db | FileCheck --check-prefix=CHECK-BRANCH %s +// RUN: %klee-exec-tree depths %t.klee-out | FileCheck --check-prefix=CHECK-DEPTH %s +// RUN: %klee-exec-tree instructions %t.klee-out | FileCheck --check-prefix=CHECK-INSTR %s +// RUN: %klee-exec-tree terminations %t.klee-out | FileCheck --check-prefix=CHECK-TERM %s +// RUN: %klee-exec-tree tree-dot %t.klee-out | FileCheck --check-prefix=CHECK-DOT %s +// RUN: %klee-exec-tree tree-info %t.klee-out | FileCheck --check-prefix=CHECK-TINFO %s +// RUN: not %klee-exec-tree dot %t.klee-out/exec-tree-doesnotexist.db #include "klee/klee.h" @@ -61,7 +61,7 @@ int main(void) { // CHECK-TERM-DAG: User,2 // CHECK-TERM-DAG: SilentExit,2 -// CHECK-DOT: strict digraph PTree { +// CHECK-DOT: strict digraph ExecutionTree { // CHECK-DOT: node[shape=point,width=0.15,color=darkgrey]; // CHECK-DOT: edge[color=darkgrey]; // CHECK-DOT-DAG: N{{[0-9]+}}[tooltip="Conditional\nnode: {{[0-9]+}}\nstate: 0\nasm: {{[0-9]+}}"]; diff --git a/test/lit.cfg b/test/lit.cfg index 8abf7012..52869d34 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -139,7 +139,7 @@ if len(kleaver_extra_params) != 0: # If a tool's name is a prefix of another, the longer name has # to come first, e.g., klee-replay should come before klee subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), - ('%klee-ptree', 'klee-ptree', ''), + ('%klee-exec-tree', 'klee-exec-tree', ''), ('%klee-replay', 'klee-replay', ''), ('%klee-stats', 'klee-stats', ''), ('%klee-zesti', 'klee-zesti', ''), |