From c9c14199edc93c5c74d184501dc52184becda0ad Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sat, 7 Oct 2023 00:42:55 +0400 Subject: [PATCH] [chore] Z3 is not required in a lot of tests, so remove the requirements --- .../LazyInitialization/DerefSymbolicPointer.c | 3 +-- .../ImpossibleAddressForLI.c | 3 +-- .../LazyInitialization/LazyInitialization.c | 3 +-- test/Feature/LazyInitialization/LinkedList.c | 3 +-- .../LazyInitialization/PointerOffset.c | 3 +-- .../SingleInitializationAndAccess.c | 3 +-- .../TwoObjectsInitialization.c | 3 +-- test/Industry/AssignNull_Scene_BadCase02.c | 1 - test/Industry/AssignNull_Scene_BadCase04.c | 1 - test/Industry/BadCase01_SecB_ForwardNull.c | 1 - test/Industry/CheckNull_Scene_BadCase02.c | 1 - test/Industry/CheckNull_Scene_BadCase04.c | 1 - test/Industry/FN_SecB_ForwardNull_filed.c | 12 +++++------ .../Industry/FN_SecB_ForwardNull_filed.c.json | 6 +++--- ...Var_Alloc_in_Loop_Exit_in_Loop_BadCase01.c | 1 - test/Industry/NullReturn_BadCase_WhiteBox01.c | 10 +++++----- .../NullReturn_BadCase_WhiteBox01.c.json | 20 +++++++++---------- test/Industry/NullReturn_Scene_BadCase01.c | 1 - test/Industry/NullReturn_Scene_BadCase02.c | 1 - test/Industry/NullReturn_Scene_BadCase03.c | 1 - test/Industry/NullReturn_Scene_BadCase04.c | 1 - test/Industry/NullReturn_Scene_BadCase06.c | 1 - test/Industry/NullReturn_Scene_BadCase08.cpp | 1 - test/Industry/SecB_ForwardNull.c | 10 +++++----- test/Industry/SecB_ForwardNull.c.json | 6 +++--- .../UseAfterFree/Double_Free_BadCase01.c | 3 +-- .../UseAfterFree/Double_Free_BadCase02.c | 3 +-- .../Free_Not_Set_Null_BadCase02.cpp | 3 +-- .../Prod_Dereference_After_Free_BadCase01.c | 1 - test/Industry/ZeroDeref_Scene_BadCase02.c | 1 - test/Industry/ZeroDeref_Scene_BadCase05.c | 1 - test/Industry/fn_reverse_null.c | 1 - test/Industry/fp_forward_null_address.c | 1 - test/Industry/fp_null_returns_self_define.c | 1 - test/Industry/fp_null_returns_self_define2.c | 1 - test/Industry/if2.c | 1 - test/Industry/test.c | 1 - test/Industry/while_true.c | 1 - ...or2c-lazyMod.adding.1.prop1-back-serstep.c | 5 +++-- ...eplay-test-with-lazy-initialized-objects.c | 4 ++-- .../2023-10-04-email_spec0_product16.cil.c | 3 +-- ...ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c | 1 - test/regression/2023-10-06-Dubois-015.c | 5 ++++- 43 files changed, 52 insertions(+), 82 deletions(-) diff --git a/test/Feature/LazyInitialization/DerefSymbolicPointer.c b/test/Feature/LazyInitialization/DerefSymbolicPointer.c index 27fd4d1d42..b0919d56a3 100644 --- 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 index abc643eb05..f0d9f25bf6 100644 --- 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 index 74356f31b3..31e82a124e 100644 --- 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 index 9431e4ffc3..191ce3103b 100644 --- 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 index aaf3694e1c..2d0b7a4321 100644 --- 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 index 1def3a9876..4c2413aa9e 100644 --- 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 diff --git a/test/Feature/LazyInitialization/TwoObjectsInitialization.c b/test/Feature/LazyInitialization/TwoObjectsInitialization.c index ab67462f3d..957f4bd7da 100644 --- 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 diff --git a/test/Industry/AssignNull_Scene_BadCase02.c b/test/Industry/AssignNull_Scene_BadCase02.c index ecb898b0b2..55fb4b7989 100644 --- 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 index 757479e40d..6a0979278f 100644 --- 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 index 38431719b3..f72959d73c 100644 --- 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 index fc27954a53..3effb46f57 100644 --- 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 index dba74dd82a..0e9038201d 100644 --- 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 index fad10a2644..6faaf136b9 100644 --- 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 \ No newline at end of file diff --git a/test/Industry/FN_SecB_ForwardNull_filed.c.json b/test/Industry/FN_SecB_ForwardNull_filed.c.json index b54baa91f9..ec0f7d3101 100644 --- 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 index 4b77bd1b66..9a04367627 100644 --- 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 index 8ee8261adb..666c470216 100644 --- 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 \ No newline at end of file diff --git a/test/Industry/NullReturn_BadCase_WhiteBox01.c.json b/test/Industry/NullReturn_BadCase_WhiteBox01.c.json index 3372239023..42a4b510f1 100644 --- 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 index cfab0db844..45b8240318 100644 --- 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 index 7042eb01b1..d25af79653 100644 --- 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 index f24ef754b6..c4190f9bb2 100644 --- 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 index d7054e5af2..377e4b9e19 100644 --- 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 index 8ad07ac540..19b11d341b 100644 --- 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 index 07870565a0..91e6dccdf8 100644 --- 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 index ef5866afbc..e3a8334c82 100644 --- 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 \ No newline at end of file diff --git a/test/Industry/SecB_ForwardNull.c.json b/test/Industry/SecB_ForwardNull.c.json index d26344534b..ee8294c266 100644 --- a/test/Industry/SecB_ForwardNull.c.json +++ b/test/Industry/SecB_ForwardNull.c.json @@ -20,7 +20,7 @@ "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/SecB_ForwardNull.c" }, "region": { - "startLine": 133, + "startLine": 128, "startColumn": null } } @@ -33,7 +33,7 @@ "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/SecB_ForwardNull.c" }, "region": { - "startLine": 134, + "startLine": 129, "startColumn": null } } @@ -52,7 +52,7 @@ "uri": "/mnt/d/wsl-ubuntu/test2/forward_null/SecB_ForwardNull.c" }, "region": { - "startLine": 134, + "startLine": 129, "startColumn": null } } diff --git a/test/Industry/UseAfterFree/Double_Free_BadCase01.c b/test/Industry/UseAfterFree/Double_Free_BadCase01.c index cece04e8a7..57d3600faa 100644 --- a/test/Industry/UseAfterFree/Double_Free_BadCase01.c +++ b/test/Industry/UseAfterFree/Double_Free_BadCase01.c @@ -16,8 +16,8 @@ * @author xwx356597;x00407107 * */ + #include -#include //@scene 指针释放后未置空导致双重释放 void DoubleFreeBad01() @@ -36,7 +36,6 @@ void DoubleFreeBad01() free(p); // CHECK: KLEE: WARNING: 100.00% DoubleFree 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 --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/UseAfterFree/Double_Free_BadCase02.c b/test/Industry/UseAfterFree/Double_Free_BadCase02.c index e6e93818d8..be8f1c52c1 100644 --- a/test/Industry/UseAfterFree/Double_Free_BadCase02.c +++ b/test/Industry/UseAfterFree/Double_Free_BadCase02.c @@ -16,8 +16,8 @@ * @author xwx356597;x00407107 * */ + #include -#include //@scene 指针释放后未置空，有条件地再再次释放导致双重释放 void DoubleFreeBad02(int flag) @@ -39,7 +39,6 @@ void DoubleFreeBad02(int flag) } } -// 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 diff --git a/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp b/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp index 6c15434bf4..90a32d9903 100644 --- a/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp +++ b/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp @@ -17,7 +17,6 @@ * */ -#include #include #include @@ -34,6 +33,7 @@ typedef struct { int a; char *pname; }Data; + //全局变量 分支结束前要重新赋值 char *MSG = (char*)malloc(1000); @@ -75,7 +75,6 @@ int main() return 0; } -// 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 diff --git a/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c b/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c index 9c171549e9..7742d31afd 100644 --- a/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c +++ b/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c @@ -33,7 +33,6 @@ void UseAfterFree() return; } -// 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 diff --git a/test/Industry/ZeroDeref_Scene_BadCase02.c b/test/Industry/ZeroDeref_Scene_BadCase02.c index 0e65b66155..dd0fe063ac 100644 --- a/test/Industry/ZeroDeref_Scene_BadCase02.c +++ b/test/Industry/ZeroDeref_Scene_BadCase02.c @@ -38,7 +38,6 @@ void TestBad9() memcpy(pDest, p, BUFFERSIZE); // CHECK-DAG: 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 --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/ZeroDeref_Scene_BadCase05.c b/test/Industry/ZeroDeref_Scene_BadCase05.c index d094cea77b..3afb67837e 100644 --- a/test/Industry/ZeroDeref_Scene_BadCase05.c +++ b/test/Industry/ZeroDeref_Scene_BadCase05.c @@ -62,7 +62,6 @@ void TestBad18(struct STU *stu) HelpBadTest1(NULL); } -// 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/fn_reverse_null.c b/test/Industry/fn_reverse_null.c index 0e02ebc842..aff52b8f68 100644 --- a/test/Industry/fn_reverse_null.c +++ b/test/Industry/fn_reverse_null.c @@ -53,7 +53,6 @@ void TestErr4(TreeNode *head) return; } -// 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 --external-calls=all --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/fp_forward_null_address.c b/test/Industry/fp_forward_null_address.c index f39297d2a4..e090051722 100644 --- a/test/Industry/fp_forward_null_address.c +++ b/test/Industry/fp_forward_null_address.c @@ -22,7 +22,6 @@ void foo() int v = *p; // CHECK: KLEE: WARNING: 100.00% NullPointerException False 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 --max-cycles-before-stuck=150 --use-guided-search=error --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/fp_null_returns_self_define.c b/test/Industry/fp_null_returns_self_define.c index 2ed62cfb68..fa331108b6 100644 --- a/test/Industry/fp_null_returns_self_define.c +++ b/test/Industry/fp_null_returns_self_define.c @@ -1,4 +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 diff --git a/test/Industry/fp_null_returns_self_define2.c b/test/Industry/fp_null_returns_self_define2.c index f737f18cc5..6606140676 100644 --- a/test/Industry/fp_null_returns_self_define2.c +++ b/test/Industry/fp_null_returns_self_define2.c @@ -26,7 +26,6 @@ void TEST_NullReturns004(unsigned short index) sink(value); } -// 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 diff --git a/test/Industry/if2.c b/test/Industry/if2.c index d52edf529f..e41a4a0a0e 100644 --- a/test/Industry/if2.c +++ b/test/Industry/if2.c @@ -8,7 +8,6 @@ int main(int x) { return *p; } -// 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 --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-stepped-instructions=20 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc diff --git a/test/Industry/test.c b/test/Industry/test.c index 9d84770da0..5b08e0cd97 100644 --- a/test/Industry/test.c +++ b/test/Industry/test.c @@ -19,7 +19,6 @@ void TestBad8(int len) buf[0] = 'a'; // CHECK-NUM: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1 } // CHECK-UID: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 8389b1896658d867c9e15267acfe8c32 -// 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/while_true.c b/test/Industry/while_true.c index a2eebdcc0a..f0566cce12 100644 --- a/test/Industry/while_true.c +++ b/test/Industry/while_true.c @@ -8,7 +8,6 @@ int main() { return *p; } -// REQUIRES: z3 // RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc // RUN: rm -rf %t.klee-out-1 // RUN: %klee --output-dir=%t.klee-out-1 --use-guided-search=error --mock-external-calls --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=10 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc diff --git a/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c index 7a6d4ff09c..6048923249 100644 --- a/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c +++ b/test/Industry/wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c @@ -1,7 +1,8 @@ -// REQUIRES: z3 +// REQUIRES: not-msan +// Disabling msan because it times out on CI // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3 -max-memory=6008 --optimize=true --skip-not-lazy-initialized -output-source=true --output-stats=false --output-istats=false --write-xml-tests --write-ktests=false --xml-metadata-programfile=wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c --xml-metadata-programhash=a18daeacf63b42ad6e1cb490555b7cdecd71ad6e58b167ed0f5626c03bc3d772 --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error --dump-states-on-halt=false -exit-on-error-type=Assert --search=dfs --search=random-path -max-time=20 %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false -max-memory=6008 --optimize=true --skip-not-lazy-initialized -output-source=true --output-stats=false --output-istats=false --write-xml-tests --write-ktests=false --xml-metadata-programfile=wrapped_btor2c-lazyMod.adding.1.prop1-back-serstep.c --xml-metadata-programhash=a18daeacf63b42ad6e1cb490555b7cdecd71ad6e58b167ed0f5626c03bc3d772 --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --function-call-reproduce=reach_error --dump-states-on-halt=false -exit-on-error-type=Assert --search=dfs --search=random-path -max-time=20 %t1.bc 2>&1 | FileCheck -check-prefix=CHECK-VERDICT %s // RUN: test -f %t.klee-out/test000001.xml // RUN: not test -f %t.klee-out/test000001.ktest diff --git a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c index ec58f72187..66edca58dc 100644 --- a/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c +++ b/test/regression/2023-02-01-replay-test-with-lazy-initialized-objects.c @@ -1,7 +1,7 @@ -// REQUIRES: not-darwin, z3 +// REQUIRES: not-darwin // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --solver-backend=z3 --skip-not-lazy-initialized --skip-not-symbolic-objects %t.bc > %t.log +// RUN: %klee --output-dir=%t.klee-out --libc=klee --posix-runtime --skip-not-lazy-initialized --skip-not-symbolic-objects %t.bc > %t.log // RUN: test -f %t.klee-out/test000006.ktest diff --git a/test/regression/2023-10-04-email_spec0_product16.cil.c b/test/regression/2023-10-04-email_spec0_product16.cil.c index 8a4acd5c58..e407b7bbb2 100644 --- a/test/regression/2023-10-04-email_spec0_product16.cil.c +++ b/test/regression/2023-10-04-email_spec0_product16.cil.c @@ -1,7 +1,6 @@ -// REQUIRES: z3 // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --solver-backend=z3 -max-memory=6008 --optimize --skip-not-lazy-initialized -istats-write-interval=90s -exit-on-error-type=Assert --search=dfs -max-time=10s %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s +// RUN: %klee --output-dir=%t.klee-out --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --istats-write-interval=90s --exit-on-error-type=Assert --search=dfs --max-time=10s %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s // RUN find %t.klee-out -type f -name "*.assert.err" | sed 's/assert\.err/ktest/' | xargs %ktest-tool | FileCheck -check-prefix=CHECK-TEST %s // CHECK-TEST-NOT: object 20 diff --git a/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c index 9b27688a42..d08c61d74a 100644 --- a/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c +++ b/test/regression/2023-10-06-ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c @@ -1,4 +1,3 @@ -// REQUIRES: z3 // RUN: %clang -Wno-everything %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize=true --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s diff --git a/test/regression/2023-10-06-Dubois-015.c b/test/regression/2023-10-06-Dubois-015.c index f70af983b4..fccb9acd93 100644 --- a/test/regression/2023-10-06-Dubois-015.c +++ b/test/regression/2023-10-06-Dubois-015.c @@ -29,7 +29,10 @@ void abort_prog() { abort(); } int __VERIFIER_nondet_int(); -void reach_error() { abort_prog(); __assert_fail("0", "Dubois-015.c", 5, "reach_error"); } +void reach_error() { + abort_prog(); + __assert_fail("0", "Dubois-015.c", 5, "reach_error"); +} void assume(int cond) { if (!cond) abort_prog();