Add failed test in debug and temp script for build

UnitTestBot · Feb 8, 2024 · 80cc67b · 80cc67b
1 parent ba72a3e
commit 80cc67b
Show file tree

Hide file tree

Showing 32 changed files with 129 additions and 30 deletions.
diff --git a/build_debug.sh b/build_debug.sh
@@ -0,0 +1,84 @@
+#!/bin/sh
+
+# For more build options, visit
+# https://klee.github.io/build-script/
+
+
+# BASE_IMAGE: ubuntu:jammy-20230126
+# REPOSITORY: ghcr.io/klee
+# COVERAGE: 0
+# DISABLE_ASSERTIONS: 0
+# ENABLE_DOXYGEN: 0
+# ENABLE_OPTIMIZED: 1
+# ENABLE_DEBUG: 1
+# GTEST_VERSION: 1.11.0
+# KLEE_RUNTIME_BUILD: "Debug+Asserts"
+# LLVM_VERSION: 11
+# MINISAT_VERSION: "master"
+# REQUIRES_RTTI: 0
+# SOLVERS: BITWUZLA:Z3:STP
+# STP_VERSION: 2.3.3
+# TCMALLOC_VERSION: 2.9.1
+# UCLIBC_VERSION: klee_uclibc_v1.3
+# USE_TCMALLOC: 1
+# USE_LIBCXX: 1
+# Z3_VERSION: 4.8.15
+# SQLITE_VERSION: 3400100
+# BITWUZLA_VERSION: main
+# BITWUZLA_COMMIT: 80ef7cd803e1c71b5939c3eb951f1736388f7090
+# JSON_VERSION: v3.11.3
+
+# Base folder where dependencies and KLEE itself are installed
+BASE=$HOME/klee_build
+
+## KLEE Required options
+# Build type for KLEE. The options are:
+# Release
+# Release+Debug
+# Release+Asserts
+# Release+Debug+Asserts
+# Debug
+# Debug+Asserts
+# KLEE_RUNTIME_BUILD="Debug+Asserts"
+KLEE_RUNTIME_BUILD="Debug+Asserts"
+
+COVERAGE=0
+ENABLE_DOXYGEN=0
+USE_TCMALLOC=1
+TCMALLOC_VERSION=2.9.1
+USE_LIBCXX=1
+# Also required despite not being mentioned in the guide
+SQLITE_VERSION="3400100"
+
+
+## LLVM Required options
+LLVM_VERSION=14
+ENABLE_OPTIMIZED=1
+ENABLE_DEBUG=1
+DISABLE_ASSERTIONS=0
+REQUIRES_RTTI=0
+
+## Solvers Required options
+# SOLVERS=STP
+SOLVERS=BITWUZLA:Z3:STP
+
+## Google Test Required options
+GTEST_VERSION=1.11.0
+
+## json options
+JSON_VERSION=v3.11.3
+
+## UClibC Required options
+UCLIBC_VERSION=klee_uclibc_v1.3
+# LLVM_VERSION is also required for UClibC
+
+## Z3 Required options
+Z3_VERSION=4.8.15
+
+STP_VERSION=2.3.3
+MINISAT_VERSION=master
+
+BITWUZLA_VERSION=0.3.1
+BITWUZLA_COMMIT=80ef7cd803e1c71b5939c3eb951f1736388f7090
+
+BITWUZLA_COMMIT="$BITWUZLA_COMMIT" TCMALLOC_VERSION="$TCMALLOC_VERSION" BASE="$BASE" KLEE_RUNTIME_BUILD=$KLEE_RUNTIME_BUILD COVERAGE=$COVERAGE ENABLE_DOXYGEN=$ENABLE_DOXYGEN USE_TCMALLOC=$USE_TCMALLOC USE_LIBCXX=$USE_LIBCXX LLVM_VERSION=$LLVM_VERSION ENABLE_OPTIMIZED=$ENABLE_OPTIMIZED ENABLE_DEBUG=$ENABLE_DEBUG DISABLE_ASSERTIONS=$DISABLE_ASSERTIONS REQUIRES_RTTI=$REQUIRES_RTTI SOLVERS=$SOLVERS GTEST_VERSION=$GTEST_VERSION UCLIBC_VERSION=$UCLIBC_VERSION STP_VERSION=$STP_VERSION MINISAT_VERSION=$MINISAT_VERSION Z3_VERSION=$Z3_VERSION BITWUZLA_VERSION=$BITWUZLA_VERSION SQLITE_VERSION=$SQLITE_VERSION JSON_VERSION=$JSON_VERSION ./scripts/build/build.sh klee --install-system-deps
diff --git a/configs/annotations.json b/configs/annotations.json
@@ -572,6 +572,16 @@
     ],
     "properties": []
   },
+  "localtime": {
+    "name": "localtime",
+    "annotation": [
+      [
+        "InitNull::Must"
+      ],
+      []
+    ],
+    "properties": []
+  },
   "malloc": {
     "name": "malloc",
     "annotation": [

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -610,6 +610,7 @@ llvm::Module *Executor::setModule(
 
     std::vector<std::unique_ptr<llvm::Module>> mockModules;
     mockModules.push_back(std::move(mockModule));
+    // std::swap(mockModule, kmodule->module);
     kmodule->link(mockModules, 1);
 
     for (auto &global : kmodule->module->globals()) {

diff --git a/test/Industry/AssignNull_Scene_BadCase02.c b/test/Industry/AssignNull_Scene_BadCase02.c
@@ -51,6 +51,6 @@ void TestBad5(struct STU *pdev, const char *buf, unsigned int count)
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --annotations=%annotations --mock-policy=all --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
 // CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 2
diff --git a/test/Industry/AssignNull_Scene_BadCase04.c b/test/Industry/AssignNull_Scene_BadCase04.c
@@ -52,5 +52,5 @@ int TestBad7(char *arg, unsigned int count)
 
 // 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-policy=failed --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
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/BadCase01_SecB_ForwardNull.c b/test/Industry/BadCase01_SecB_ForwardNull.c
@@ -142,6 +142,6 @@ void badbad(char *ptr)
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc > %t1.log 2>&1
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc > %t1.log 2>&1
 // RUN: FileCheck -input-file=%t1.log %s
 // CHECK: KLEE: WARNING: No paths were given to trace verify
diff --git a/test/Industry/CheckNull_Scene_BadCase02.c b/test/Industry/CheckNull_Scene_BadCase02.c
@@ -43,5 +43,5 @@ void TestBad2()
 
 // 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-policy=failed --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=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
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/CheckNull_Scene_BadCase04.c b/test/Industry/CheckNull_Scene_BadCase04.c
@@ -58,5 +58,5 @@ void TestBad12(int cond1, int cond2)
 
 // 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-policy=failed --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=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
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/FN_SecB_ForwardNull_filed.c b/test/Industry/FN_SecB_ForwardNull_filed.c
@@ -47,5 +47,5 @@ void WB_BadCase_field2(DataInfo *data)
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c b/test/Industry/MemoryLeak/LocalVar_Alloc_in_Loop_Exit_in_Loop_BadCase01.c
@@ -55,7 +55,7 @@ void call_func(int num)
 
 // 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-policy=failed --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --write-kqueries --max-cycles-before-stuck=0 --use-guided-search=error  --annotations=%annotations --mock-policy=all --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
 
 // CHECK: KLEE: WARNING: 100.00% Reachable Reachable at trace 1
diff --git a/test/Industry/NullReturn_BadCase_WhiteBox01.c b/test/Industry/NullReturn_BadCase_WhiteBox01.c
@@ -66,5 +66,5 @@ void NullReturn_BadCase_WhiteBox01(UINT8 index, SchedHarqStru *harqInfo)
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --smart-resolve-entry-function --use-guided-search=error --annotations=%annotations --mock-policy=all --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_Scene_BadCase01.c b/test/Industry/NullReturn_Scene_BadCase01.c
@@ -41,5 +41,5 @@ void TestBad1()
 
 // 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-policy=failed --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
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/NullReturn_Scene_BadCase02.c b/test/Industry/NullReturn_Scene_BadCase02.c
@@ -40,5 +40,5 @@ void TestBad2()
 
 // 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-policy=failed --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
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --location-accuracy --annotations=%annotations --mock-policy=all  --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_Scene_BadCase03.c b/test/Industry/NullReturn_Scene_BadCase03.c
@@ -42,5 +42,5 @@ void TestBad3()
 
 // 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-policy=failed --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=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
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/NullReturn_Scene_BadCase04.c b/test/Industry/NullReturn_Scene_BadCase04.c
@@ -46,6 +46,6 @@ void TestBad4()
 
 // 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-policy=failed --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --annotations=%annotations --mock-policy=all --libc=klee --external-calls=all --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
 // CHEK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1
diff --git a/test/Industry/NullReturn_Scene_BadCase06.c b/test/Industry/NullReturn_Scene_BadCase06.c
@@ -54,7 +54,7 @@ void TestBad6(unsigned int count)
 
 // 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-policy=failed --check-out-of-memory --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --check-out-of-memory --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
 
 // CHECK-DAG: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 1

diff --git a/test/Industry/NullReturn_Scene_BadCase08.cpp b/test/Industry/NullReturn_Scene_BadCase08.cpp
@@ -39,6 +39,6 @@ void TestBad9()
 
 // 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-policy=failed --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --write-kqueries --use-guided-search=error --location-accuracy --annotations=%annotations --mock-policy=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
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
 // CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 2
diff --git a/test/Industry/SecB_ForwardNull.c b/test/Industry/SecB_ForwardNull.c
@@ -131,5 +131,5 @@ void badbad(char *ptr)
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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/UseAfterFree/Double_Free_BadCase01.c b/test/Industry/UseAfterFree/Double_Free_BadCase01.c
@@ -38,5 +38,5 @@ void DoubleFreeBad01()
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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/UseAfterFree/Double_Free_BadCase02.c b/test/Industry/UseAfterFree/Double_Free_BadCase02.c
@@ -41,5 +41,5 @@ void DoubleFreeBad02(int flag)
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp b/test/Industry/UseAfterFree/Free_Not_Set_Null_BadCase02.cpp
@@ -77,7 +77,7 @@ int main()
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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
 
 // CHECK: KLEE: WARNING: 100.00% UseAfterFree False Positive at trace 1
diff --git a/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c b/test/Industry/UseAfterFree/Prod_Dereference_After_Free_BadCase01.c
@@ -35,5 +35,5 @@ void UseAfterFree()
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --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/ZeroDeref_Scene_BadCase02.c b/test/Industry/ZeroDeref_Scene_BadCase02.c
@@ -40,5 +40,5 @@ void TestBad9()
 
 // 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-policy=failed --check-out-of-memory --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=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
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
diff --git a/test/Industry/ZeroDeref_Scene_BadCase05.c b/test/Industry/ZeroDeref_Scene_BadCase05.c
@@ -64,7 +64,7 @@ void TestBad18(struct STU *stu)
 
 // 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-policy=failed --libc=klee --external-calls=all --skip-not-symbolic-objects --skip-not-lazy-initialized --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --check-out-of-memory --annotations=%annotations --mock-policy=all --libc=klee --external-calls=all --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
 // CHECK: KLEE: WARNING: 100.00% NullPointerException True Positive at trace 2
 // CHECK: KLEE: WARNING: 100.00% NullPointerException False Positive at trace 1
diff --git a/test/Industry/fn_reverse_null.c b/test/Industry/fn_reverse_null.c
@@ -55,5 +55,5 @@ void TestErr4(TreeNode *head)
 
 // 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-policy=failed --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
+// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --external-calls=all --annotations=%annotations --mock-policy=all --libc=klee --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
 // RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s