[klee-dev] Klee options

2014-07-29 Thread Zhiyi Zhang
--posix-runtime --use-independent-solver ./echo.bc --sym-arg 3* If these options are not right, could you tell me which options were used when you did the experiment in the paper OSDI08? I am very interesting in Klee. Hope for your reply as soon as possible. Thank you very much. Zhiyi Zhang

[klee-dev] Fwd: Install Problems for LLVM2.9

2015-01-29 Thread Zhiyi Zhang
* *But I did find LLVM-LD in my computer, because I downloaded the LLVM-3.4 with the order sudo apt-get install clang-3.4 llvm-3.4 llvm-3.4-dev llvm-3.4-tools. Also I did not found librt in my computer.* Thank you. Zhiyi Zhang ___ klee-dev mailing list klee

Re: [klee-dev] coreutils on KLEE3.4

2015-03-18 Thread Zhiyi Zhang
? And after make order, can the Coreutils6.11 be compiled completely？ Thank you very much. Zhiyi Zhang On Wed, Mar 18, 2015 at 4:57 PM, Dan Liew d...@su-root.co.uk wrote: Hi Zhiyi, Please do reply-all when using the mailing list so that klee-dev gets CC'ed. On 18 March 2015 at 08:32, Zhiyi Zhang

[klee-dev] coreutils on KLEE3.4

2015-03-17 Thread Zhiyi Zhang
the path of sys/cdefs.h in makefile, but the errors are the same. *So what can I do to solve these problems? Or the coreutils could only work on KLEE2.9?* Thank you very much. Zhiyi Zhang ___ klee-dev mailing list klee-dev@imperial.ac.uk https

[klee-dev] whole-program-llvm

2015-03-19 Thread Zhiyi Zhang
there are some errors in my steps? Thank you very much. Zhiyi Zhang ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[klee-dev] Executing Coreutils Error

2015-03-27 Thread Zhiyi Zhang
at this location* *Segmentation fault (core dumped)* What should I do to solve these problems? Thank you very much! Zhiyi Zhang ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] whole-program-llvm

2015-03-19 Thread Zhiyi Zhang
)* * File /home/loveling10/whole-program-llvm-master/extract-bc, line 79, in getSectionSizeAndOffset* *filename)* *Exception: Could not find .llvm_bc ELF section in /home/loveling10/klee/examples/coreutils/coreutils/obj-llvm/src/base64* Thank you very much, Zhiyi Zhang On Thu, Mar 19, 2015 at 5

[klee-dev] Klee Coverage Information

2015-04-30 Thread Zhiyi Zhang
*klee-replay *and *gcov*. But when I used *gcov*, such as *gcov echo*, the error message is *echo.gcno: cannot open notes file* I have* .cvc* files, *.cov *files and *.ktest* files generated by Klee, so how I get the coverage information only for source files? Thank you! Zhiyi Zhang

[klee-dev] Coverage Information

2015-05-04 Thread Zhiyi Zhang
*klee-replay *and *gcov*. But when I used *gcov*, such as *gcov echo*, the error message is *echo.gcno: cannot open notes file* I have* .cvc* files, *.cov *files and *.ktest* files generated by Klee, so how I get the coverage information only for source files? Thank you! Zhiyi Zhang

[klee-dev] Statement and Branch Coverage

2015-05-06 Thread Zhiyi Zhang
-coreutils/)* . But when I used *gcov*, such as* gcov echo*, the error message is *echo.gcda: cannot open data file assuming not executed* I have* .cvc* files, *.cov *files and *.ktest* files generated by Klee, so how I get the statement coverage information only for source files? Thank you! Zhiyi Zhang

[klee-dev] Experssion Rewriter

2015-05-11 Thread Zhiyi Zhang
Hi all, When I used klee with llvm3.4, I found that there is no --rewrite option in klee orders. So how could I use expression rewrite optimization when I use klee running a program? Thank you. Zhiyi Zhang ___ klee-dev mailing list klee-dev

Re: [klee-dev] Experssion Rewriter

2015-05-11 Thread Zhiyi Zhang
I see it. Thank you very much. Best wishes! Zhiyi Zhang On Mon, May 11, 2015 at 7:54 PM, Eric Rizzi eric.ri...@gmail.com wrote: There should be a --rewrite-equalities option per the following commit https://github.com/klee/klee/commit/f0de5e4ea4f1bed2e698ae99a19f1f0b96770f9c The default

[klee-dev] Klee Replay Error

2015-05-19 Thread Zhiyi Zhang
inputs*, and* sometimes these test cases could all pass*. Moreover, I replay these test case one by one, there is also no error. I do not know whether this is a bug of klee. Hope my feedback has some help of klee's development. Best wishes. Zhiyi Zhang

Re: [klee-dev] Path Search Heuristics

2015-05-26 Thread Zhiyi Zhang
could help me! Thank you. Zhiyi Zhang On Mon, May 25, 2015 at 3:16 PM, gwpub...@wp.pl wrote: It's explained in paper, Also for exercise I recommend you to try to explore graph of possible states of few simple programs (some execution path leading to infinite loop, recursion) and you should see

[klee-dev] Path Search Heuristics

2015-05-24 Thread Zhiyi Zhang
execution. Thank you! Zhiyi Zhang ___ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Path Search Heuristics

2015-05-24 Thread Zhiyi Zhang
or nurs:depth, KLEE runs OK. 2, Why KLEE uses interleaved searcher? Is interleaved search heuristic better than single search heuristic for symbolic execution? Best wishes! Zhiyi Zhang, On Mon, May 25, 2015 at 5:20 AM, Sean Bartell s...@yotann.org wrote: Zhiyi Zhang on 2015-05-24: 1

[klee-dev] Klee-uclibc.bca Error when Running Coreutils

2017-05-06 Thread Zhiyi Zhang
e as following, *KLEE: ERROR: Link with library /home/jcklee/jc/jcnewklee/klee/Release+Asserts/lib/klee-uclibc.bca failed: Invalid valueLoading module failed : Invalid value* Could you give me some suggestions to solve this problem? Thank you very much. Best wishes