From 36a9acc3880861842cc6a9da11dd872e36ed19cb Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 2 Nov 2018 14:49:03 +0000 Subject: Added test for the case where external calls are encountered but disallowed --- test/Feature/NoExternalCallsAllowed.c | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test/Feature/NoExternalCallsAllowed.c (limited to 'test') diff --git a/test/Feature/NoExternalCallsAllowed.c b/test/Feature/NoExternalCallsAllowed.c new file mode 100644 index 00000000..a0886121 --- /dev/null +++ b/test/Feature/NoExternalCallsAllowed.c @@ -0,0 +1,13 @@ +// RUN: %llvmgcc %s -emit-llvm %O0opt -c -g -o %t1.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --external-calls=none %t1.bc 2>&1 | FileCheck %s +// RUN: test %t.klee-out/test000001.user.err + +#include + +int main(int argc, char** argv) { + // CHECK: Disallowed call to external function: abs + int x = abs(argc); + printf("%d\n", argc); + return 0; +} -- cgit 1.4.1