about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-12-22 18:22:02 +0200
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-12 12:00:35 +0000
commit3fa03d12d28658694f2bf2085e8634cc267e3f16 (patch)
treec775b6d770c98ca310e9caf50c36016f99b81891 /test
parent2c8b74cc858793c94e5476b5765e93ee23738702 (diff)
downloadklee-3fa03d12d28658694f2bf2085e8634cc267e3f16.tar.gz
Renamed PTree to ExecutionTree (and similar)
Diffstat (limited to 'test')
-rw-r--r--test/CMakeLists.txt2
-rw-r--r--test/Feature/KleeExecTreeBogus.test50
-rw-r--r--test/Feature/WriteExecutionTree.c18
-rw-r--r--test/lit.cfg2
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', ''),