diff --git a/lib/Core/Composer.cpp b/lib/Core/Composer.cpp index 975a8ad1e8..9b59d791de 100644 --- a/lib/Core/Composer.cpp +++ b/lib/Core/Composer.cpp @@ -221,6 +221,17 @@ ExprVisitor::Action ComposeVisitor::visitSelect(const SelectExpr &select) { processSelect(select.cond, select.trueExpr, select.falseExpr)); } +ExprVisitor::Action +ComposeVisitor::visitPointer(const PointerExpr &pointerExpr) { + return Action::changeTo(processPointer(pointerExpr.base, pointerExpr.value)); +} + +ref ComposeVisitor::processPointer(ref base, ref value) { + auto trueBase = visit(base)->getValue(); + auto trueValue = visit(value)->getValue(); + return PointerExpr::create(trueBase, trueValue); +} + ref ComposeVisitor::shareUpdates(ref os, const UpdateList &updates) { ref copy(new ObjectState(*os.get())); diff --git a/lib/Core/Composer.h b/lib/Core/Composer.h index c514dbe402..b7cd068c3f 100644 --- a/lib/Core/Composer.h +++ b/lib/Core/Composer.h @@ -200,6 +200,9 @@ class ComposeVisitor : public ExprVisitor { ExprVisitor::Action visitRead(const ReadExpr &) override; ExprVisitor::Action visitConcat(const ConcatExpr &concat) override; ExprVisitor::Action visitSelect(const SelectExpr &) override; + ExprVisitor::Action visitPointer(const PointerExpr &) override; + + ref processPointer(ref base, ref value); ref processRead(const Array *root, const UpdateList &updates, ref index, Expr::Width width); ref processSelect(ref cond, ref trueExpr, diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 3b7cfe4ca7..acf19ba949 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -167,9 +167,9 @@ ExecutionState::ExecutionState(const ExecutionState &state) forkDisabled(state.forkDisabled), isolated(state.isolated), finalComposing(state.finalComposing), returnValue(state.returnValue), gepExprBases(state.gepExprBases), multiplexKF(state.multiplexKF), - prevTargets_(state.prevTargets_), targets_(state.targets_), - prevHistory_(state.prevHistory_), history_(state.history_), - isTargeted_(state.isTargeted_) { + localObjects(state.localObjects), prevTargets_(state.prevTargets_), + targets_(state.targets_), prevHistory_(state.prevHistory_), + history_(state.history_), isTargeted_(state.isTargeted_) { queryMetaData.id = state.id; } diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index 8e030b5449..3906d642c7 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -405,6 +405,9 @@ class ExecutionState { // Temp: to know which multiplex path this state has taken KFunction *multiplexKF = nullptr; + // set with reads from alloca instructions + std::set> localObjects; + private: PersistentSet> prevTargets_; PersistentSet> targets_; diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 9ba03fd78c..a4e7c127b5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -5391,6 +5391,7 @@ void Executor::run(ExecutionState *initialState, } else if (ExecutionMode == ExecutionKind::Bidirectional) { InitializerPredicate *predicate = new TraceVerifyPredicate( data.specialPoints, *codeGraphInfo.get(), InitializeInJoinBlocks); + // object manager assumes ownership over predicate objectManager->setPredicate(predicate); auto initializer = createIsolatedStatesInitializer(predicate, data); isolatedStatesInitializer = initializer.get(); @@ -7380,8 +7381,10 @@ void Executor::lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf, ref id = lazyInitializeObject( state, pointer, target, elementSize, size, true, conditionExpr, state.isolated || UseSymbolicSizeLazyInit); - state.addPointerResolution(pointer, id.get()); - state.addPointerResolution(basePointer, id.get()); + if (!state.isolated) { + state.addPointerResolution(pointer, id.get()); + state.addPointerResolution(basePointer, id.get()); + } state.addConstraint(EqExpr::create(address, id->getBaseExpr())); state.addConstraint( Expr::createIsZero(EqExpr::create(address, Expr::createPointer(0)))); @@ -7390,6 +7393,14 @@ void Executor::lazyInitializeLocalObject(ExecutionState &state, StackFrame &sf, } RefObjectPair op = state.addressSpace.findOrLazyInitializeObject(id.get()); state.addressSpace.bindObject(op.first, op.second.get()); + if (state.localObjects.count(id) == 0) { + for (auto localObject : state.localObjects) { + auto localObjectAddress = localObject->getBaseExpr(); + state.constraints.addConstraint(Expr::createIsZero( + EqExpr::create(id->getBaseExpr(), localObjectAddress))); + } + state.localObjects.insert(id); + } } void Executor::lazyInitializeLocalObject(ExecutionState &state, diff --git a/lib/Core/ObjectManager.h b/lib/Core/ObjectManager.h index 241be1138d..00c5f7538e 100644 --- a/lib/Core/ObjectManager.h +++ b/lib/Core/ObjectManager.h @@ -116,7 +116,7 @@ class ObjectManager { std::vector subscribers; PForest *processForest; - InitializerPredicate *predicate; + std::unique_ptr predicate; public: ExecutionState *emptyState; @@ -164,7 +164,7 @@ class ObjectManager { } void setPredicate(InitializerPredicate *predicate_) { - predicate = predicate_; + predicate = std::unique_ptr(predicate_); } }; diff --git a/lib/Solver/BitwuzlaBuilder.cpp b/lib/Solver/BitwuzlaBuilder.cpp index b39f23eddd..c8ef69d98f 100644 --- a/lib/Solver/BitwuzlaBuilder.cpp +++ b/lib/Solver/BitwuzlaBuilder.cpp @@ -1113,6 +1113,11 @@ Term BitwuzlaBuilder::constructActual(ref e, int *width_out) { assert(*width_out != 1 && "uncanonicalized FNeg"); return ctx->mk_term(Kind::FP_NEG, {arg}); } + case Expr::Pointer: + case Expr::ConstantPointer: { + PointerExpr *pointerExpr = cast(e); + return constructActual(pointerExpr->getValue(), width_out); + }; // unused due to canonicalization #if 0 @@ -1124,7 +1129,7 @@ case Expr::Sge: #endif default: - assert(0 && "unhandled Expr type"); + klee_error("unhandled Expr type"); return getTrue(); } } diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index aa32b70b05..8cda0a93ad 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -658,7 +658,7 @@ MetaSMTBuilder::constructActual(ref e, int *width_out) { switch (e->getKind()) { case Expr::Pointer: case Expr::ConstantPointer: { - assert(0 && "unreachable"); + return constructActual(e->getValue(), width_out); } case Expr::Constant: { diff --git a/lib/Solver/Z3BitvectorBuilder.cpp b/lib/Solver/Z3BitvectorBuilder.cpp index 9127f4848d..1a59444091 100644 --- a/lib/Solver/Z3BitvectorBuilder.cpp +++ b/lib/Solver/Z3BitvectorBuilder.cpp @@ -273,7 +273,8 @@ Z3ASTHandle Z3BitvectorBuilder::constructActual(ref e, int *width_out) { switch (e->getKind()) { case Expr::Pointer: case Expr::ConstantPointer: { - assert(0 && "unreachable"); + auto ptrExpr = cast(e); + return constructActual(ptrExpr->getValue(), width_out); } case Expr::Constant: { diff --git a/lib/Solver/Z3CoreBuilder.cpp b/lib/Solver/Z3CoreBuilder.cpp index 74bf166e3a..e131070d0d 100644 --- a/lib/Solver/Z3CoreBuilder.cpp +++ b/lib/Solver/Z3CoreBuilder.cpp @@ -206,7 +206,7 @@ Z3ASTHandle Z3CoreBuilder::constructActual(ref e, int *width_out) { switch (e->getKind()) { case Expr::Pointer: case Expr::ConstantPointer: { - assert(0 && "unreachable"); + return constructActual(e->getValue(), width_out); } case Expr::Constant: { diff --git a/test/Bidirectional/Memory/cond-function-pointer-change-2.c b/test/Bidirectional/Memory/cond-function-pointer-change-2.c new file mode 100644 index 0000000000..016be8bec6 --- /dev/null +++ b/test/Bidirectional/Memory/cond-function-pointer-change-2.c @@ -0,0 +1,36 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *km, int *kn, int inner_toggle) { + if (inner_toggle == 1) { + *km = 0; + } else { + *kn = 0; + } +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + klee_assume(toggle == 0 || toggle == 1); + M(&m, &n, toggle); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/cond-function-pointer-change-3.c b/test/Bidirectional/Memory/cond-function-pointer-change-3.c new file mode 100644 index 0000000000..ca13176312 --- /dev/null +++ b/test/Bidirectional/Memory/cond-function-pointer-change-3.c @@ -0,0 +1,36 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *km, int *kn, int inner_toggle) { + if (inner_toggle == 1) { + *km = 0; + } else { + *kn = 0; + } +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + M(&m, &n, toggle); + klee_assume(toggle == 1); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/cond-function-pointer-change.c b/test/Bidirectional/Memory/cond-function-pointer-change.c new file mode 100644 index 0000000000..c84236279d --- /dev/null +++ b/test/Bidirectional/Memory/cond-function-pointer-change.c @@ -0,0 +1,38 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + klee_assume(toggle == 0 || toggle == 1); + int *ptr; + if (toggle == 0) { + ptr = &m; + } else { + ptr = &n; + } + M(ptr); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/cond-stack-pointer-change.c b/test/Bidirectional/Memory/cond-stack-pointer-change.c new file mode 100644 index 0000000000..b3bc698949 --- /dev/null +++ b/test/Bidirectional/Memory/cond-stack-pointer-change.c @@ -0,0 +1,34 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int n = 3; + int toggle; + klee_make_symbolic(&toggle, sizeof(toggle), "toggle"); + klee_assume(toggle == 0 || toggle == 1); + int *ptr; + if (toggle == 0) { + ptr = &m; + } else { + ptr = &n; + } + *ptr = 0; + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/double-alloc-call-possible.c b/test/Bidirectional/Memory/double-alloc-call-possible.c new file mode 100644 index 0000000000..bb2aaa1476 --- /dev/null +++ b/test/Bidirectional/Memory/double-alloc-call-possible.c @@ -0,0 +1,31 @@ +// XFAIL: true +// do not support good symbolic memory currently +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=3 --max-stack-frames=4 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --use-visitor-hash=false --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int *my_alloca() { + int *a = malloc(sizeof(int)); + return a; +} + +int main() { + int *x = my_alloca(); + int *y = my_alloca(); + if (y != x) { + reach_error(); + } + free(x); + free(y); +} + +// CHECK: [TRUE POSITIVE] diff --git a/test/Bidirectional/Memory/fake-function-pointer-change.c b/test/Bidirectional/Memory/fake-function-pointer-change.c new file mode 100644 index 0000000000..6e6fbcdc39 --- /dev/null +++ b/test/Bidirectional/Memory/fake-function-pointer-change.c @@ -0,0 +1,30 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + int n = 4; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int *ptr = &n; + M(ptr); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/fake-stack-pointer-change.c b/test/Bidirectional/Memory/fake-stack-pointer-change.c new file mode 100644 index 0000000000..0aaf5e9720 --- /dev/null +++ b/test/Bidirectional/Memory/fake-stack-pointer-change.c @@ -0,0 +1,26 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int main() { + int m; + int n = 4; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int *ptr = &n; + *ptr = 0; + if (m != 0) { + reach_error(); + } +} + +// CHECK: [TRUE POSITIVE] FOUND TRUE POSITIVE AT diff --git a/test/Bidirectional/Memory/function-pointer-assign-change.c b/test/Bidirectional/Memory/function-pointer-assign-change.c new file mode 100644 index 0000000000..e48e65f868 --- /dev/null +++ b/test/Bidirectional/Memory/function-pointer-assign-change.c @@ -0,0 +1,29 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int *ptr = &m; + M(ptr); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/function-pointer-change.c b/test/Bidirectional/Memory/function-pointer-change.c new file mode 100644 index 0000000000..00dd9b5c0d --- /dev/null +++ b/test/Bidirectional/Memory/function-pointer-change.c @@ -0,0 +1,28 @@ +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void M(int *k) { + *k = 0; +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + M(&m); + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/stack-pointer-change-2.c b/test/Bidirectional/Memory/stack-pointer-change-2.c new file mode 100644 index 0000000000..3b67520ac1 --- /dev/null +++ b/test/Bidirectional/Memory/stack-pointer-change-2.c @@ -0,0 +1,36 @@ +// REQUIRES: not-metasmt +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +void f() { + int n = 0; +} + +int main() { + int m; + int *n = &m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(m != 0); + int k; + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k == 0); + f(); + if (k == 0) { + *n = 0; + } + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT diff --git a/test/Bidirectional/Memory/stack-pointer-change.c b/test/Bidirectional/Memory/stack-pointer-change.c new file mode 100644 index 0000000000..e2b19b8fd4 --- /dev/null +++ b/test/Bidirectional/Memory/stack-pointer-change.c @@ -0,0 +1,28 @@ +// checks that symbolic memory works in bidirectional mode +// it does not; requires a fix + +// RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log +// RUN: FileCheck %s -input-file=%t.log + +#include "klee/klee.h" +#include +#include + +void reach_error() { + klee_assert(0); +} + +int main() { + int m; + klee_make_symbolic(&m, sizeof(m), "m"); + klee_assume(0 < m && m < 10000); + int *ptr = &m; + *ptr = 0; + if (m != 0) { + reach_error(); + } +} + +// CHECK: [FALSE POSITIVE] FOUND FALSE POSITIVE AT 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 500b9febc3..6849ace74d 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,4 +1,4 @@ -// REQUIRES: not-darwin +// REQUIRES: not-darwin, posix // 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 --skip-not-lazy-initialized --min-number-elements-li=4 %t.bc > %t.log