[klee-dev] Problems with Klee Docker Image

[Andrea Mattavelli]

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-paris at 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 at 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 at 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 at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev <https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
-------------- next part --------------
HTML attachment scrubbed and removed