Dear Paris,
you are encountering a common C problem: you are using a function before it is
declared. In this case, since the function klee_make_symbolic is external, it
means that you forgot to include the header file “klee/klee.h”.
To summarize, your test case should be the following:
#include"klee/klee.h"
int diff(int x, int y) {
int diff;
diff = x - y;
if (diff > 127) {
diff = 127;
} else if (diff < -127) {
diff = -127;
}
return diff;
}
int main() {
int x;
int y;
klee_make_symbolic(&x, sizeof(x), "x");
klee_make_symbolic(&y, sizeof(y), "y");
diff(x, y);
}
Andrea
> On 20 Feb 2016, at 18:18, Paris Tamiolakis <tamiolakis-pa...@hotmail.com>
> wrote:
>
> Hello everyone,
>
> My name is Paris Tamiolakis. I am a student of informatics and I am having
> problems with an assignment concerning Klee. I am trying to run klee from a
> docker image but having problems when my code includes the function
> klee_make_symbolic. The code that I use is the same as the gentlemans in the
> link below.
>
> https://github.com/klee/klee/issues/285
> <https://github.com/klee/klee/issues/285>
>
> The results that I end with are the following:
>
> After compilation:
> klee@4f6d6445f44b <https://webmail.aueb.gr/imp/dynamic.php?page=mailbox#>:~$
> clang -emit-llvm -g -c test4.c -o test4.bc
> test4.c:3:3: warning: implicit declaration of function 'klee_make_symbolic'
> is invalid in C99 [-Wimplicit-function-declaration]
> klee_make_symbolic(&a, sizeof(a), a);
> ^
> 1 warning generated.
>
> After run:
> klee@4f6d6445f44b <https://webmail.aueb.gr/imp/dynamic.php?page=mailbox#>:~$
> klee --libc=uclibc test4.bc
> KLEE: NOTE: Using klee-uclibc :
> /home/klee/klee_build/klee/Release+Asserts/lib/klee-uclibc.bca
> KLEE: output directory is "/home/klee/klee-out-6"
> Using STP solver backend
> KLEE: WARNING: undefined reference to function: fcntl
> KLEE: WARNING: undefined reference to function: fstat
> KLEE: WARNING: undefined reference to function: ioctl
> KLEE: WARNING: undefined reference to function: open
> KLEE: WARNING: undefined reference to function: write
> KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 63609152)
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
> klee: /home/klee/klee_src/lib/Core/SpecialFunctionHandler.cpp:242:
> std::string
> klee::SpecialFunctionHandler::readStringAtAddress(klee::ExecutionState &,
> ref<klee::Expr>): Assertion `0 && "XXX out of bounds / multiple resolution
> unhandled"' failed.
> 0 klee 0x0000000000dcab02 llvm::sys::PrintStackTrace(_IO_FILE*) +
> 34
> 1 klee 0x0000000000dca8f4
> 2 libpthread.so.0 0x00002b2ba020a340
> 3 libc.so.6 0x00002b2ba26aecc9 gsignal + 57
> 4 libc.so.6 0x00002b2ba26b20d8 abort + 328
> 5 libc.so.6 0x00002b2ba26a7b86
> 6 libc.so.6 0x00002b2ba26a7c32
> 7 klee 0x000000000059dab9
> 8 klee 0x00000000005a0675
> klee::SpecialFunctionHandler::handleMakeSymbolic(klee::ExecutionState&,
> klee::KInstruction*, std::vector<klee::ref<klee::Expr>,
> std::allocator<klee::ref<klee::Expr> > >&) + 117
> 9 klee 0x000000000059d665
> klee::SpecialFunctionHandler::handle(klee::ExecutionState&, llvm::Function*,
> klee::KInstruction*, std::vector<klee::ref<klee::Expr>,
> std::allocator<klee::ref<klee::Expr> > >&) + 197
> 10 klee 0x000000000057ddb8
> klee::Executor::callExternalFunction(klee::ExecutionState&,
> klee::KInstruction*, llvm::Function*, std::vector<klee::ref<klee::Expr>,
> std::allocator<klee::ref<klee::Expr> > >&) + 88
> 11 klee 0x000000000057d067
> klee::Executor::executeCall(klee::ExecutionState&, klee::KInstruction*,
> llvm::Function*, std::vector<klee::ref<klee::Expr>,
> std::allocator<klee::ref<klee::Expr> > >&) + 119
> 12 klee 0x000000000058135f
> klee::Executor::executeInstruction(klee::ExecutionState&,
> klee::KInstruction*) + 4751
> 13 klee 0x0000000000589ccc
> klee::Executor::run(klee::ExecutionState&) + 1180
> 14 klee 0x000000000058ce17
> klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 2039
> 15 klee 0x0000000000573b34 main + 13860
> 16 libc.so.6 0x00002b2ba2699ec5 __libc_start_main + 245
> 17 klee 0x000000000056c859
> Aborted (core dumped)
>
> If u have any idea what is the problem, or how I could fix it, I would very
> much appreciate it. Thank you in advance.
>
> Yours sincerely,
> Paris Tamiolakis
>
>
> Το παρόν email στάλθηκε από ασφαλή υπολογιστή που προστατεύεται από το Avast.
> www.avast.com <https://www.avast.com/sig-email>
> <x-msg://46/#DDB4FAA8-2DD7-40BB-A1B8-4E2AA1F9FDF2>_______________________________________________
> klee-dev mailing list
> klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
