Re: [klee-dev] How to avoid calling the solver if the branch is known at run-time

2018-05-04 Thread Andrew Santosa
Hi Charitha, I think you would need to do the modification in Executor::fork(). You would notice within that function there is the following three lines: solver->setTimeout(timeout); bool success = solver->evaluate(current, condition, res); solver->setTimeout(0); I would try to replace those

Re: [klee-dev] Unable to build Klee with LLVM 3.8

2018-05-04 Thread Cristian Cadar
Hi Sang, We plan to merge #729 into the mainline soon. However, the other PR, #605, still needs some work. But I hope to be able to bring support for 3.8 into the mainline in the next few weeks. Best, Cristian On 04/05/2018 22:44, Sang Phan wrote: Hello, I'm using a newer Ubuntu where

[klee-dev] Unable to build Klee with LLVM 3.8

2018-05-04 Thread Sang Phan
Hello, I'm using a newer Ubuntu where LLVM 3.4 is no longer available. So I'm trying to build Klee with LLVM 3.8 following the instructions in this link: http://klee.github.io/build-llvm38/ However, I couldn't merge the pull request. After running git merge pull729 I got the following errors:

[klee-dev] How to avoid calling the solver if the branch is known at run-time

2018-05-04 Thread Charitha Saumya
Hi, I want to implement a search strategy in KLEE. If I know some branch is feasible from prior knowledge (say I learn that for a some br instruction the true branch is always feasible), How can I change KLEE to avoid calling the solver in Executor.cpp (in Instruction::Br) and just guide

Re: [klee-dev] Space program in KLEE

2018-05-04 Thread Norlina Pasaribu
Hallo there, I just tried Klee I Mac, and I using this command but command not found. is this command only for linux ? or any suggestion for iMac ? Thank you very much ITs-iMac-7:Test Space itdel$ klee -posix-runtime -libc=uclibc -max-time=60 ./space.bc A -sym-files 1 10 -bash: klee: command