[chore] Z3 is not required in a lot of tests, so remove the requirements

UnitTestBot · Oct 6, 2023 · b0c4f14 · b0c4f14
1 parent 85b5f35
commit b0c4f14
Show file tree

Hide file tree

Showing 43 changed files with 47 additions and 79 deletions.
diff --git a/test/Feature/LazyInitialization/DerefSymbolicPointer.c b/test/Feature/LazyInitialization/DerefSymbolicPointer.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --write-kqueries --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t.bc > %t.log
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 #include "klee/klee.h"
 

diff --git a/test/Feature/LazyInitialization/ImpossibleAddressForLI.c b/test/Feature/LazyInitialization/ImpossibleAddressForLI.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 

diff --git a/test/Feature/LazyInitialization/LazyInitialization.c b/test/Feature/LazyInitialization/LazyInitialization.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// 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
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --use-guided-search=none %t.bc > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 
 struct Node {

diff --git a/test/Feature/LazyInitialization/LinkedList.c b/test/Feature/LazyInitialization/LinkedList.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --write-kqueries --solver-backend=z3 --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --skip-not-symbolic-objects %t.bc > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 #include "klee/klee.h"
 

diff --git a/test/Feature/LazyInitialization/PointerOffset.c b/test/Feature/LazyInitialization/PointerOffset.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects --use-timestamps=false --skip-local=false %t.bc
 // RUN: %ktest-tool %t.klee-out/test*.ktest > %t.log
 // RUN: FileCheck %s -input-file=%t.log
 // CHECK: pointers: [(0, 1, 4)]

diff --git a/test/Feature/LazyInitialization/SingleInitializationAndAccess.c b/test/Feature/LazyInitialization/SingleInitializationAndAccess.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// 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
+// 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
 
 #include "klee/klee.h"
 #include <assert.h>

diff --git a/test/Feature/LazyInitialization/TwoObjectsInitialization.c b/test/Feature/LazyInitialization/TwoObjectsInitialization.c
@@ -1,7 +1,6 @@
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -g -c -o %t1.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --skip-not-symbolic-objects %t1.bc 2>&1 | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --skip-not-symbolic-objects %t1.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>

diff --git a/test/Industry/AssignNull_Scene_BadCase02.c b/test/Industry/AssignNull_Scene_BadCase02.c
@@ -49,7 +49,6 @@ void TestBad5(struct STU *pdev, const char *buf, unsigned int count)
     printf("teacher id is %ud", teacherID);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // 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

diff --git a/test/Industry/AssignNull_Scene_BadCase04.c b/test/Industry/AssignNull_Scene_BadCase04.c
@@ -50,7 +50,6 @@ int TestBad7(char *arg, unsigned int count)
     return 1;
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // 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

diff --git a/test/Industry/BadCase01_SecB_ForwardNull.c b/test/Industry/BadCase01_SecB_ForwardNull.c
@@ -140,7 +140,6 @@ void badbad(char *ptr)
 }
 #endif
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // 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

diff --git a/test/Industry/CheckNull_Scene_BadCase02.c b/test/Industry/CheckNull_Scene_BadCase02.c
@@ -41,7 +41,6 @@ void TestBad2()
     free(errMsg);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // 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 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/CheckNull_Scene_BadCase04.c b/test/Industry/CheckNull_Scene_BadCase04.c
@@ -56,7 +56,6 @@ void TestBad12(int cond1, int cond2)
 	}
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // 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 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/FN_SecB_ForwardNull_filed.c b/test/Industry/FN_SecB_ForwardNull_filed.c
@@ -1,8 +1,3 @@
-// REQUIRES: z3
-// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
-// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
 /*
  * Copyright (c) Huawei Technologies Co., Ltd. 2021-2021. All rights reserved.
  * @description 空指针解引用 验收失败
@@ -44,8 +39,13 @@ void WB_BadCase_Field(UINT32 inputNum1, UINT32 inputNum2)
 void WB_BadCase_field2(DataInfo *data)
 {
   data->dataBuff = NULL;
-  *data->dataBuff = 'c'; // CHECK: KLEE: WARNING: 100.00% NullPointerException False Negative at: {{.*}}test/Industry/FN_SecB_ForwardNull_filed.c:47 19
+  *data->dataBuff = 'c'; // CHECK: KLEE: WARNING: 100.00% NullPointerException False Negative at: {{.*}}test/Industry/FN_SecB_ForwardNull_filed.c:42 19
 
   char *ptr = NULL;
   *ptr = 'c'; // CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 1
 }
+
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/FN_SecB_ForwardNull_filed.c.json b/test/Industry/FN_SecB_ForwardNull_filed.c.json
@@ -20,7 +20,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/./FN_SecB_ForwardNull_filed.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 49,
+                                                        "startLine": 44,
                                                         "startColumn": null
                                                     }
                                                 }
@@ -33,7 +33,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/./FN_SecB_ForwardNull_filed.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 50,
+                                                        "startLine": 45,
                                                         "startColumn": null
                                                     }
                                                 }
@@ -52,7 +52,7 @@
                                     "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/./FN_SecB_ForwardNull_filed.c"
                                 },
                                 "region": {
-                                    "startLine": 50,
+                                    "startLine": 45,
                                     "startColumn": null
                                 }
                             }

diff --git a/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c
@@ -53,7 +53,6 @@ void call_func(int num)
     ResourceLeak_bad01(num);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --write-kqueries --max-cycles-before-stuck=0 --use-guided-search=error --check-out-of-memory --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/NullReturn_BadCase_WhiteBox01.c b/test/Industry/NullReturn_BadCase_WhiteBox01.c
@@ -1,8 +1,3 @@
-// REQUIRES: z3
-// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --smart-resolve-entry-function --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
-// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
 /*
  * Copyright (c) Huawei Technologies Co., Ltd. 2022-2022. All rights reserved.
  *
@@ -68,3 +63,8 @@ void NullReturn_BadCase_WhiteBox01(UINT8 index, SchedHarqStru *harqInfo)
         SendMsg(index, usrId, resultInfo);                                                              // (3)
     }
 }
+
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --smart-resolve-entry-function --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/NullReturn_BadCase_WhiteBox01.c.json b/test/Industry/NullReturn_BadCase_WhiteBox01.c.json
@@ -20,7 +20,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 45,
+                                                        "startLine": 40,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -33,7 +33,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 66,
+                                                        "startLine": 61,
                                                         "startColumn": 34
                                                     }
                                                 }
@@ -46,7 +46,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 68,
+                                                        "startLine": 63,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -59,7 +59,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 56,
+                                                        "startLine": 51,
                                                         "startColumn": 30
                                                     }
                                                 }
@@ -78,7 +78,7 @@
                                     "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                 },
                                 "region": {
-                                    "startLine": 56,
+                                    "startLine": 51,
                                     "startColumn": 30
                                 }
                             }
@@ -98,7 +98,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 45,
+                                                        "startLine": 40,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -111,7 +111,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 66,
+                                                        "startLine": 61,
                                                         "startColumn": 34
                                                     }
                                                 }
@@ -124,7 +124,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 68,
+                                                        "startLine": 63,
                                                         "startColumn": 9
                                                     }
                                                 }
@@ -137,7 +137,7 @@
                                                         "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                                     },
                                                     "region": {
-                                                        "startLine": 54,
+                                                        "startLine": 49,
                                                         "startColumn": 30
                                                     }
                                                 }
@@ -156,7 +156,7 @@
                                     "uri": "/mnt/d/wsl-ubuntu/test2/null_returns/NullReturn_BadCase_WhiteBox01.c"
                                 },
                                 "region": {
-                                    "startLine": 54,
+                                    "startLine": 49,
                                     "startColumn": 30
                                 }
                             }

diff --git a/test/Industry/NullReturn_Scene_BadCase01.c b/test/Industry/NullReturn_Scene_BadCase01.c
@@ -39,7 +39,6 @@ void TestBad1()
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --external-calls=all --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/NullReturn_Scene_BadCase02.c b/test/Industry/NullReturn_Scene_BadCase02.c
@@ -38,7 +38,6 @@ void TestBad2()
     printf("The second is %d", info->tm_sec); // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --mock-external-calls --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --extern-calls-can-return-null --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/NullReturn_Scene_BadCase03.c b/test/Industry/NullReturn_Scene_BadCase03.c
@@ -40,7 +40,6 @@ void TestBad3()
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // 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 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/NullReturn_Scene_BadCase04.c b/test/Industry/NullReturn_Scene_BadCase04.c
@@ -44,7 +44,6 @@ void TestBad4()
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --mock-external-calls --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/NullReturn_Scene_BadCase06.c b/test/Industry/NullReturn_Scene_BadCase06.c
@@ -52,7 +52,6 @@ void TestBad6(unsigned int count)
     free(buf);
 }
 
-// REQUIRES: z3
 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/NullReturn_Scene_BadCase08.cpp b/test/Industry/NullReturn_Scene_BadCase08.cpp
@@ -37,7 +37,6 @@ void TestBad9()
 	printf("the current integer is: %d", *p); // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }
 
-// REQUIRES: z3
 // RUN: %clangxx %s -emit-llvm %O0opt -c -g -o %t1.bc
 // RUN: rm -rf %t.klee-out
 // RUN: %klee --output-dir=%t.klee-out --write-kqueries --use-guided-search=error --location-accuracy --mock-external-calls --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc

diff --git a/test/Industry/SecB_ForwardNull.c b/test/Industry/SecB_ForwardNull.c
@@ -1,8 +1,3 @@
-// REQUIRES: z3
-// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
-// RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
-// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
 /*
  * Copyright (c) Huawei Technologies Co., Ltd. 2021-2021. All rights reserved.
  * @description 空指针解引用 验收失败
@@ -133,3 +128,8 @@ void badbad(char *ptr)
   ptr = NULL;
   *ptr = 'a'; // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
 }
+
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --mock-external-calls --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s