diff --git a/lib/Core/MockBuilder.cpp b/lib/Core/MockBuilder.cpp index 5c82feee13..7d2b9ddb09 100644 --- a/lib/Core/MockBuilder.cpp +++ b/lib/Core/MockBuilder.cpp @@ -139,7 +139,7 @@ std::unique_ptr MockBuilder::build() { loadFileAsOneModule(extFile, ctx, loadedUserModules, errorMsg); std::swap(loadedUserModules.front(), mockModule); - auto mainFn = mockModule->getFunction(opts.MainCurrentName); + auto mainFn = mockModule->getFunction(opts.EntryPoint); mainFn->setName(opts.MainCurrentName); } diff --git a/test/regression/2024-08-29-mock-with-posix.c b/test/regression/2024-08-29-mock-with-posix.c new file mode 100644 index 0000000000..23c5ec6ff3 --- /dev/null +++ b/test/regression/2024-08-29-mock-with-posix.c @@ -0,0 +1,24 @@ +// REQUIRES: posix-runtime +// REQUIRES: z3 + +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc + +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --mock-policy=all --posix-runtime --external-calls=all %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK +// CHECK: ASSERTION FAIL +// CHECK: KLEE: done: completed paths = 2 +// CHECK: KLEE: done: generated tests = 3 + +#include + +extern int foo(int x, int y); + +int main() { + int a, b; + klee_make_symbolic(&a, sizeof(a), "a"); + klee_make_symbolic(&b, sizeof(b), "b"); + if (a == b && foo(a + b, b) != foo(2 * b, a)) { + assert(0); + } + return 0; +}