Skip to content

Commit c9c1419

Browse files
misonijnikmisonijnik
committed
[chore] Z3 is not required in a lot of tests, so remove the requirements
1 parent d5095be commit c9c1419

43 files changed

Lines changed: 52 additions & 82 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎test/Feature/LazyInitialization/DerefSymbolicPointer.c‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
// REQUIRES: z3
21
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
32
// RUN: rm -rf %t.klee-out
4-
// RUN: %klee --write-kqueries --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t.bc > %t.log
3+
// RUN: %klee --write-kqueries --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
54
// RUN: FileCheck %s -input-file=%t.log
65
#include "klee/klee.h"
76

‎test/Feature/LazyInitialization/ImpossibleAddressForLI.c‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
// REQUIRES: z3
21
// RUN: %clang %s -emit-llvm -g -c -o %t.bc
32
// RUN: rm -rf %t.klee-out
4-
// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t.bc 2>&1 | FileCheck %s
3+
// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc 2>&1 | FileCheck %s
54

65
#include "klee/klee.h"
76

‎test/Feature/LazyInitialization/LazyInitialization.c‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
// REQUIRES: z3
21
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
32
// RUN: rm -rf %t.klee-out
4-
// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --use-timestamps=false --use-guided-search=none %t.bc > %t.log
3+
// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --use-guided-search=none %t.bc > %t.log
54
// RUN: FileCheck %s -input-file=%t.log
65

76
struct Node {

‎test/Feature/LazyInitialization/LinkedList.c‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
// REQUIRES: z3
21
// RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
32
// RUN: rm -rf %t.klee-out
4-
// RUN: %klee --write-kqueries --solver-backend=z3 --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
3+
// RUN: %klee --write-kqueries --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
54
// RUN: FileCheck %s -input-file=%t.log
65
#include "klee/klee.h"
76

‎test/Feature/LazyInitialization/PointerOffset.c‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
// REQUIRES: z3
21
// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
32
// RUN: rm -rf %t.klee-out
4-
// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc
3+
// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc
54
// RUN: %ktest-tool %t.klee-out/test*.ktest > %t.log
65
// RUN: FileCheck %s -input-file=%t.log
76
// CHECK: pointers: [(0, 1, 4)]

‎test/Feature/LazyInitialization/SingleInitializationAndAccess.c‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
// REQUIRES: z3
21
// RUN: %clang %s -emit-llvm -g -c -o %t1.bc
32
// RUN: rm -rf %t.klee-out
4-
// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --skip-local=false --use-sym-size-li --min-number-elements-li=1 %t1.bc 2>&1 | FileCheck %s
3+
// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --skip-local=false --use-sym-size-li --min-number-elements-li=1 %t1.bc 2>&1 | FileCheck %s
54

65
#include "klee/klee.h"
76
#include <assert.h>

‎test/Feature/LazyInitialization/TwoObjectsInitialization.c‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
// REQUIRES: z3
21
// RUN: %clang %s -emit-llvm -g -c -o %t1.bc
32
// RUN: rm -rf %t.klee-out
4-
// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t1.bc 2>&1 | FileCheck %s
3+
// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t1.bc 2>&1 | FileCheck %s
54

65
#include "klee/klee.h"
76
#include <assert.h>

‎test/Industry/AssignNull_Scene_BadCase02.c‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,6 @@ void TestBad5(struct STU *pdev, const char *buf, unsigned int count)
4949
printf("teacher id is %ud", teacherID);
5050
}
5151

52-
// REQUIRES: z3
5352
// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
5453
// RUN: rm -rf %t.klee-out
5554
// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

‎test/Industry/AssignNull_Scene_BadCase04.c‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,6 @@ int TestBad7(char *arg, unsigned int count)
5050
return 1;
5151
}
5252

53-
// REQUIRES: z3
5453
// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
5554
// RUN: rm -rf %t.klee-out
5655
// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --smart-resolve-entry-function --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

‎test/Industry/BadCase01_SecB_ForwardNull.c‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -140,7 +140,6 @@ void badbad(char *ptr)
140140
}
141141
#endif
142142

143-
// REQUIRES: z3
144143
// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
145144
// RUN: rm -rf %t.klee-out
146145
// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

0 commit comments

Comments
 (0)