diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 31 | ||||
| -rw-r--r-- | test/CXX/ArrayNew.cpp | 2 | ||||
| -rw-r--r-- | test/CXX/New.cpp | 2 | ||||
| -rw-r--r-- | test/CXX/SimpleVirtual.cpp | 2 | ||||
| -rw-r--r-- | test/Feature/LowerSwitch.c | 4 | ||||
| -rw-r--r-- | test/Runtime/POSIX/MixedConcreteSymbolic.c | 2 |
6 files changed, 25 insertions, 18 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ddf11929..099123cd 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -103,11 +103,6 @@ namespace { cl::init(true), cl::desc("Dump test cases for all active states on exit (default=on)")); - cl::opt<bool> - AllowExternalSymCalls("allow-external-sym-calls", - cl::init(false), - cl::desc("Allow calls with symbolic arguments to external functions. This concretizes the symbolic arguments. (default=off)")); - /// The different query logging solvers that can switched on/off enum PrintDebugInstructionsType { STDERR_ALL, /// @@ -185,10 +180,21 @@ namespace { cl::init(false), cl::desc("Generate tests cases for all errors " "(default=off, i.e. one per (error,instruction) pair)")); - - cl::opt<bool> - NoExternals("no-externals", - cl::desc("Do not allow external function calls (default=off)")); + + enum class ExternalCallPolicy { + None, // No external calls allowed + Concrete, // Only external calls with concrete arguments allowed + All, // All external calls allowed + }; + + cl::opt<ExternalCallPolicy> + ExternalCalls("external-calls", + cl::desc("Specify the external call policy"), + cl::values(clEnumValN(ExternalCallPolicy::None, "none", "No external function calls are allowed. Note that KLEE always allows some external calls with concrete arguments to go through (in particular printf and puts), regardless of this option."), + clEnumValN(ExternalCallPolicy::Concrete, "concrete", "Only external function calls with concrete arguments are allowed (default)"), + clEnumValN(ExternalCallPolicy::All, "all", "All external function calls are allowed. This concretizes any symbolic arguments in calls to external functions.") + KLEE_LLVM_CL_VAL_END), + cl::init(ExternalCallPolicy::Concrete)); cl::opt<bool> AlwaysOutputSeeds("always-output-seeds", @@ -3099,10 +3105,11 @@ void Executor::callExternalFunction(ExecutionState &state, if (specialFunctionHandler->handle(state, function, target, arguments)) return; - if (NoExternals && !okExternals.count(function->getName())) { + if (ExternalCalls == ExternalCallPolicy::None + && !okExternals.count(function->getName())) { klee_warning("Disallowed call to external function: %s\n", function->getName().str().c_str()); - terminateStateOnError(state, "externals disallowed", User); + terminateStateOnError(state, "external calls disallowed", User); return; } @@ -3115,7 +3122,7 @@ void Executor::callExternalFunction(ExecutionState &state, unsigned wordIndex = 2; for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), ae = arguments.end(); ai!=ae; ++ai) { - if (AllowExternalSymCalls) { // don't bother checking uniqueness + if (ExternalCalls == ExternalCallPolicy::All) { // don't bother checking uniqueness *ai = optimizer.optimizeExpr(*ai, true); ref<ConstantExpr> ce; bool success = solver->getValue(state, *ai, ce); diff --git a/test/CXX/ArrayNew.cpp b/test/CXX/ArrayNew.cpp index baad95fe..35a4f134 100644 --- a/test/CXX/ArrayNew.cpp +++ b/test/CXX/ArrayNew.cpp @@ -1,6 +1,6 @@ // 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 +// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --external-calls=none %t1.bc #include <cassert> diff --git a/test/CXX/New.cpp b/test/CXX/New.cpp index 71784f9f..921316a7 100644 --- a/test/CXX/New.cpp +++ b/test/CXX/New.cpp @@ -1,6 +1,6 @@ // 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 +// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --external-calls=none %t1.bc #include <cassert> diff --git a/test/CXX/SimpleVirtual.cpp b/test/CXX/SimpleVirtual.cpp index 7d0faa08..372b44de 100644 --- a/test/CXX/SimpleVirtual.cpp +++ b/test/CXX/SimpleVirtual.cpp @@ -1,6 +1,6 @@ // 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 +// RUN: %klee --output-dir=%t.klee-out --no-output --exit-on-error --external-calls=none %t1.bc #include <cassert> diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c index 1b280e72..faa82365 100644 --- a/test/Feature/LowerSwitch.c +++ b/test/Feature/LowerSwitch.c @@ -1,10 +1,10 @@ // RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --external-calls=all --switch-type=internal %t.bc // RUN: not test -f %t.klee-out/test000010.ktest // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc +// RUN: %klee --output-dir=%t.klee-out --exit-on-error --switch-type=simple %t.bc // RUN: test -f %t.klee-out/test000010.ktest #include <stdio.h> diff --git a/test/Runtime/POSIX/MixedConcreteSymbolic.c b/test/Runtime/POSIX/MixedConcreteSymbolic.c index c32a8f54..71abb116 100644 --- a/test/Runtime/POSIX/MixedConcreteSymbolic.c +++ b/test/Runtime/POSIX/MixedConcreteSymbolic.c @@ -1,6 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out -allow-external-sym-calls --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-stdin 10 2>%t.log | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --external-calls=all --exit-on-error --libc=uclibc --posix-runtime %t.bc --sym-stdin 10 2>%t.log | FileCheck %s #include "klee/klee.h" #include <assert.h> |