Skip to content

Commit

Permalink
llvm5: test, add -disable-O0-optnone to -O0
Browse files Browse the repository at this point in the history
Otherwise optimizations done in klee won't have any effect.

Signed-off-by: Jiri Slaby <[email protected]>
  • Loading branch information
jirislaby authored and MartinNowack committed Oct 26, 2018
1 parent 1f15695 commit 0a7963e
Show file tree
Hide file tree
Showing 135 changed files with 147 additions and 137 deletions.
8 changes: 7 additions & 1 deletion runtime/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -91,13 +91,19 @@ ExternalProject_Add(BuildKLEERuntimes
INSTALL_COMMAND "${CMAKE_COMMAND}" -E echo "" # Dummy command
)

set(O0OPT "-O0")
if (${LLVM_VERSION_MAJOR} GREATER 4)
set(O0OPT "${O0OPT} -Xclang -disable-O0-optnone")
endif()


# Use `ExternalProject_Add_Step` with `ALWAYS` argument instead of directly
# building in `ExternalProject_Add` with `BUILD_ALWAYS` argument due to lack of
# support for the `BUILD_ALWAYS` argument in CMake < 3.1.
ExternalProject_Add_Step(BuildKLEERuntimes RuntimeBuild
# `env` is used here to make sure `MAKEFLAGS` of KLEE's build
# is not propagated into the bitcode build system.
COMMAND ${ENV_BINARY} MAKEFLAGS="" ${MAKE_BINARY} -f Makefile.cmake.bitcode all
COMMAND ${ENV_BINARY} MAKEFLAGS="" O0OPT=${O0OPT} ${MAKE_BINARY} -f Makefile.cmake.bitcode all
ALWAYS ${EXTERNAL_PROJECT_BUILD_ALWAYS_ARG}
WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}"
${EXTERNAL_PROJECT_ADD_STEP_USES_TERMINAL_ARG}
Expand Down
2 changes: 1 addition & 1 deletion runtime/Makefile.cmake.bitcode.rules
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ endif
ifeq ($(IS_RELEASE),1)
LLVMCC.Flags += -O2
else
LLVMCC.Flags += -O0
LLVMCC.Flags += $(O0OPT)
endif

# Handle assertion flags
Expand Down
2 changes: 1 addition & 1 deletion test/CXX/ArrayNew.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgxx %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --no-externals %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/CXX/New.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgxx %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --no-externals %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/CXX/SimpleVirtual.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgxx %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --no-externals %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/CXX/StaticConstructor.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgxx %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/CXX/StaticDestructor.cpp
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
// don't optimize this, llvm likes to turn the *p into unreachable

// RUN: %llvmgxx %s -emit-llvm -g -O0 -c -o %t1.bc
// RUN: %llvmgxx %s -emit-llvm -g %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --optimize=false --libc=klee --no-output %t1.bc 2> %t1.log
// RUN: FileCheck --input-file %t1.log %s
Expand Down
2 changes: 1 addition & 1 deletion test/CXX/Trivial.cpp
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgxx %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgxx %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/Coverage/ReadArgs.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: echo " --output-dir=%t.klee-out " > %t1.args
// RUN: %klee @%t1.args %t1.bc
Expand Down
2 changes: 1 addition & 1 deletion test/Coverage/ReplayOutDir.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t1.out %t1.replay
// RUN: %klee --output-dir=%t1.out %t1.bc
// RUN: %klee --output-dir=%t1.replay --replay-ktest-dir=%t1.out %t1.bc
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/AliasFunction.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
// RUN: grep -c foo %t1.log | grep 5
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/AliasFunctionExit.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
// RUN: grep -c START %t1.log | grep 1
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/ByteSwap.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee --exit-on-error %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/CheckForImpliedValue.c.failing
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -f %t1.log
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --log-file %t1.log --debug-check-for-implied-values %t1.bc
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/CompressedExprLogging.c
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// REQUIRES: zlib
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t1.bc
// We disable the cex-cache to eliminate nondeterminism across different
// solvers, in particular when counting the number of queries in the last two
// commands
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/DanglingConcreteReadExpr.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --optimize=false --output-dir=%t.klee-out %t1.bc
// RUN: grep "total queries = 2" %t.klee-out/info
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/DoubleFree.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
// RUN: test -f %t.klee-out/test000001.ptr.err
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/DumpStatesOnHalt.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc 2>&1 | FileCheck %s
// RUN: test -f %t.klee-out/test000001.ktest
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/ExitOnErrorType.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -exit-on-error-type Assert %t1.bc 2>&1

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/ExprLogging.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t1.bc
// We disable the cex-cache to eliminate nondeterminism across different solvers, in particular when counting the number of queries in the last two commands
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --use-cex-cache=false --use-query-log=all:kquery,all:smt2,solver:kquery,solver:smt2 --write-kqueries --write-cvcs --write-smt2s %t1.bc 2> %t2.log
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/FloatingPt.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/InAndOutOfBounds.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
// RUN: test -f %t.klee-out/test000001.ptr.err -o -f %t.klee-out/test000002.ptr.err
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/IsSymbolic.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/KleeReportError.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t2.bc 2>&1 | FileCheck %s
// RUN: ls %t.klee-out/ | grep .my.err | wc -l | grep 2
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/LargeReturnTypes.cpp
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// REQUIRES: not-darwin
// RUN: %llvmgxx -g -fno-exceptions -emit-llvm -O0 -c -o %t.bc %s
// RUN: %llvmgxx -g -fno-exceptions -emit-llvm %O0opt -c -o %t.bc %s
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log

Expand Down
4 changes: 2 additions & 2 deletions test/Feature/LinkLLVMLib.c
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc -DLINK_LLVM_LIB_TEST_LIB
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc -DLINK_LLVM_LIB_TEST_LIB
// RUN: %llvmar r %t1.a %t1.bc
//
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t2.bc -DLINK_LLVM_LIB_TEST_EXEC
// RUN: rm -rf %t.klee-out
// RUN: %klee --link-llvm-lib %t1.a --output-dir=%t.klee-out --emit-all-errors --warnings-only-to-file=false %t2.bc 2>&1 | FileCheck %s

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/LongDouble.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc -g -emit-llvm -O0 -c -o %t.bc %s
// RUN: %llvmgcc -g -emit-llvm %O0opt -c -o %t.bc %s
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee --no-output --exit-on-error %t.bc > %t.log
// RUN: FileCheck %s --input-file=%t.log
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/LongDoubleSupport.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --optimize=0 --exit-on-error %t1.bc > %t2.out

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/MultipleFreeResolution.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --emit-all-errors %t1.bc 2>&1 | FileCheck %s
// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/MultipleReadResolution.c
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// RUN: echo "x" >> %t1.res
// RUN: echo "x" >> %t1.res
// RUN: echo "x" >> %t1.res
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
// RUN: diff %t1.res %t1.log
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/MultipleReallocResolution.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc
// RUN: ls %t.klee-out/ | grep .err | wc -l | grep 2
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/MultipleWriteResolution.c
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// RUN: echo "x" >> %t1.res
// RUN: echo "x" >> %t1.res
// RUN: echo "x" >> %t1.res
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc > %t1.log
// RUN: diff %t1.res %t1.log
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/OneFreeError.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
// RUN: test -f %t.klee-out/test000001.ptr.err
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/OneOutOfBounds.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s
// RUN: test -f %t.klee-out/test000001.ptr.err
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/Optimize.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t2.bc
// RUN: rm -f %t2.log
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --stop-after-n-instructions=100 --optimize %t2.bc > %t3.log
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/OverlappedError.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -g -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t1.bc
// RUN: ls %t.klee-out/ | grep .ktest | wc -l | grep 4
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/OvershiftCheck.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -check-overshift %t.bc 2> %t.log
// RUN: FileCheck --input-file %t.log %s
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/PreferCex.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
// RUN: ktest-tool %t.klee-out/test000001.ktest | FileCheck %s
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/RaiseAsm.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/Realloc.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --exit-on-error --warnings-only-to-file=false %t1.bc 2>&1 | FileCheck %s

Expand Down
4 changes: 2 additions & 2 deletions test/Feature/ReplayPath.c
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -DCOND_EXIT -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -DCOND_EXIT -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --write-paths %t1.bc > %t3.good

// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t2.bc
// RUN: rm -rf %t.klee-out-2
// RUN: %klee --output-dir=%t.klee-out-2 --replay-path %t.klee-out/test000001.path %t2.bc > %t3.log
// RUN: diff %t3.log %t3.good
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/RewriteEqualities.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --search=dfs --write-kqueries --rewrite-equalities=false %t.bc
// RUN: grep "N0:(Read w8 2 x)" %t.klee-out/test000003.kquery
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/Searchers.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t2.bc
// RUN: rm -rf %t.klee-out
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/SolverTimeout.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --max-solver-time=1 %t1.bc
// FIXME: This test occasionally fails when using Z3 4.4.1 but
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/SourceMapping.c
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Check that we properly associate instruction level statistics with source
// file and line.
//
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc
// RUN: FileCheck < %t.klee-out/run.istats %s
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/VarArgLongDouble.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t.bc | FileCheck %s

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/Vararg.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -g -o %t1.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -g -o %t1.bc
// RUN: rm -rf %t.klee-out
// This test needs deterministic allocation with enough spacing between the allocations.
// Otherwise, if by coincidence the allocated vararg memory object is directly before another valid memory object,
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/WithLibc.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t2.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee %t2.bc > %t3.log
// RUN: echo "good" > %t3.good
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/arithmetic-right-overshift-sym-conc.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc
// RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/consecutive_divide_by_zero.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc -emit-llvm -c -g -O0 %s -o %t.bc
// RUN: %llvmgcc -emit-llvm -c -g %O0opt %s -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log
// RUN: FileCheck --input-file=%t.log %s
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/const_array_opt1.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --const-array-opt --max-time=10 --only-output-states-covering-new %t.bc >%t.log
// grep -q "Finished successfully!\n"
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/left-overshift-sym-conc.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc
// RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/logical-right-overshift-sym-conc.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 -check-overshift=0 %t.bc
// RUN: not grep "ASSERTION FAIL" %t.klee-out/messages.txt
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/srem.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out -use-cex-cache=1 %t.bc
// RUN: grep "KLEE: done: explored paths = 5" %t.klee-out/info
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/ubsan_signed_overflow.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -fsanitize=signed-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc %s -fsanitize=signed-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s

Expand Down
2 changes: 1 addition & 1 deletion test/Feature/ubsan_unsigned_overflow.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc %s -fsanitize=unsigned-integer-overflow -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc %s -fsanitize=unsigned-integer-overflow -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s

Expand Down
2 changes: 1 addition & 1 deletion test/Programs/pcregrep.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc -m32 %s -emit-llvm -O0 -c -o %t1.bc
// RUN: %llvmgcc -m32 %s -emit-llvm %O0opt -c -o %t1.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee --exit-on-error %t1.bc 2 2
// XFAIL: x86_64
Expand Down
2 changes: 1 addition & 1 deletion test/Replay/libkleeruntest/replay_invalid_klee_assume.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc -DASSUME_VALUE=1 %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc -DASSUME_VALUE=1 %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc
// RUN: test -f %t.klee-out/test000001.ktest
Expand Down
2 changes: 1 addition & 1 deletion test/Replay/libkleeruntest/replay_invalid_klee_choose.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc
// RUN: test -f %t.klee-out/test000001.ktest
Expand Down
2 changes: 1 addition & 1 deletion test/Replay/libkleeruntest/replay_invalid_klee_range.c
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %llvmgcc -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g -O0 -c -o %t.bc
// RUN: %llvmgcc -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g %O0opt -c -o %t.bc
// RUN: rm -rf %t.klee-out
// RUN: %klee --output-dir=%t.klee-out --libc=klee --search=dfs %t.bc
// RUN: test -f %t.klee-out/test000001.ktest
Expand Down
Loading

0 comments on commit 0a7963e

Please sign in to comment.