Skip to content

Commit

Permalink
fix:
Browse files Browse the repository at this point in the history
  • Loading branch information
misonijnik committed Aug 20, 2024
1 parent 476f821 commit 8430a13
Show file tree
Hide file tree
Showing 6 changed files with 6 additions and 6 deletions.
2 changes: 1 addition & 1 deletion test/Industry/UseAfterFree/Double_Free_BadCase01.c
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ void DoubleFreeBad01()
free(p); // CHECK: KLEE: WARNING: 100.00% DoubleFree True Positive at trace 1
}

// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -Wno-implicit-function-declaration -o %t1.bc
// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
// RUN: rm -rf %t.klee-out
// 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
2 changes: 1 addition & 1 deletion test/Industry/UseAfterFree/Double_Free_BadCase02.c
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ void DoubleFreeBad02(int flag)
}
}

// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -Wno-implicit-function-declaration -o %t1.bc
// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
// RUN: rm -rf %t.klee-out
// 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
2 changes: 1 addition & 1 deletion test/Industry/if2.c
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ int main(int x) {
return *p;
}

// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -Wno-implicit-function-declaration -o %t1.bc
// RUN: %clang %s -emit-llvm %O0opt -c -g -O0 -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --use-guided-search=error --annotations=%annotations --mock-policy=all --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --search=bfs --max-cycles=1 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NONE
Expand Down
2 changes: 1 addition & 1 deletion test/Industry/test.c
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ 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

// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -Wno-implicit-function-declaration -o %t1.bc
// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc
// RUN: rm -rf %t.klee-out
// 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
// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s -check-prefix=CHECK-NUM
Expand Down
2 changes: 1 addition & 1 deletion test/Industry/while_true.c
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ int main() {
return *p;
}

// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -Wno-implicit-function-declaration -o %t1.bc
// RUN: %clang %s -emit-llvm %O0opt -c -g -O0 -o %t1.bc
// RUN: rm -rf %t.klee-out-1
// RUN: %klee --output-dir=%t.klee-out-1 --use-guided-search=error --mock-policy=failed --skip-not-symbolic-objects --skip-not-lazy-initialized --check-out-of-memory --max-stepped-instructions=20 --max-cycles-before-stuck=0 --use-lazy-initialization=only --analysis-reproduce=%s.json %t1.bc
// RUN: FileCheck -input-file=%t.klee-out-1/warnings.txt %s -check-prefix=CHECK-NONE
Expand Down
2 changes: 1 addition & 1 deletion test/lit.site.cfg.in
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ config.cxx = "@NATIVE_CXX@"

# NOTE: any changes to compiler flags also have to be applied to
# test/Concrete/CMakeLists.txt
config.O0opt = "-O0 -Xclang -disable-O0-optnone"
config.O0opt = "-O0 -Xclang -disable-O0-optnone -Wno-implicit-function-declaration"

config.sqlite3 = "@SQLITE_CLI@"

Expand Down

0 comments on commit 8430a13

Please sign in to comment.