Re: [klee-dev] concretized symbolic size

1:10, "klee-dev-boun...@imperial.ac.uk on behalf of Michael" sp...@pobox.com> wrote: Hi, I'm using klee for the first time and am seeing it stop with the following error: KLEE: ERROR: EXITING ON ERROR: Error: concretized symbolic size File: libc/mis

[klee-dev] concretized symbolic size

omething? Thanks for this great tool, BTW. -- Michael ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] error report empty

Hi all, I have now succesfully build klee. But if run the examples the test-N.xxx.err files are empty. What can I do? Best regards, Michael [Logo Berner und Mattner] Michael Eßer | Senior System Engineer | AUTOMOTIVE Berner Mattner Systemtechnik GmbH | Erwin-von-Kreibig-Straße 3 | 80807

[klee-dev] newbie questions to klee: .err-file - klee_assert - div by zero

regards, Michael [Logo Berner und Mattner] Michael Eßer | Senior System Engineer | AUTOMOTIVE Berner Mattner Systemtechnik GmbH | Erwin-von-Kreibig-Straße 3 | 80807 München (Germany) Tel.: +49 89 608090-417 | Fax: +49 89 60 98-182 michael.es...@berner-mattner.com mailto:michael.es...@berner

[klee-dev] compile error with klee

mailto:klee-dev@imperial.ac.ukWhen i compile klee I get the following error message: make[2]: *** Keine Regel vorhanden, um das Target »/home/michael/Downloads/klee/runtime/Intrinsic/Release+Asserts/klee_div_zero_check.ll«, benötigt von »/home/michael/Downloads/klee/runtime/Intrinsic/Release

[klee-dev] error while configuring klee

und Mattner] Michael Eßer | Senior System Engineer | AUTOMOTIVE Berner Mattner Systemtechnik GmbH | Erwin-von-Kreibig-Straße 3 | 80807 München (Germany) Tel.: +49 89 608090-417 | Fax: +49 89 60 98-182 michael.es...@berner-mattner.com mailto:michael.es...@berner-mattner.com | Infos: www.berner

[klee-dev] using klee with Siemens Benchmarks

this right?) As a result, as Paul somewhat tersely replied: what's the executable spec -- i.e., the true set of requirements from which MC/DC or other test cases might be generated? Regards, Michael P.S. - also, have you played with using Klee to check equivalence or bisimulation of two programs

Re: [klee-dev] STP compile issue for KLEE

You're missing bison. Try installing it with sudo apt-get install bison and then continue your build. Regards, Michael On 4/10/12, Changjiang Jia cjjia...@gmail.com wrote: Dear KLEE project members: I'm Changjiang, a graduate from City University of Hong Kong. I try to build KLEE on my

[klee-dev] Using Klee against shared libraries

Hi, I am trying to work out if it is possible to use shared libraries with Klee. Specifically, lets say I have an application that calls various library functions - can I mark the input to those external libraries as symbolic and execute both the library and application symbolically? I have

Re: [klee-dev] [Patch] general small fixes for Klee, motivated by compiling under Minix

locations while still permitting the same binaries and libraries to function in their installed locations without modification. Might a strategy like this one work for you too? Regards, Michael [1]: https://github.com/mstone/klee/ [2]: https://github.com/mstone/klee/commit

[klee-dev] Unable to compile klee

Daniel wrote: Make sure when you configure LLVM that it is finding an llvm-gcc which matches the same version of LLVM. This statement would be a good addition to the http://klee.llvm.org/GetStarted.html instructions. Regards, Michael