testing right now.
I had the same problem a while ago, and it turns out the correct guard
is = LLVM_VERSION(3,4). I've attached a patch.
Thanks,
Sean Bartell
From b7d1273c308a46bbe32c3c156dc70052026035d6 Mon Sep 17 00:00:00 2001
From: Sean Bartell yot...@yotann.org
Date: Mon, 22 Sep 2014 22:06:42
Zhenyu Zhou on 2015-06-20:
I'm looking for a tool for symbolic execution and find that Klee is a
fantastic tool. But now I'm wondering whether Klee can analyse JAVA codes
(or class files)? I have searched in the mail list and found the same
question is posted several years ago. Does anyone know
Hi,
Alexander Kampmann on 2015-06-25:
For my test input, the ktest-tool outputs the same object name twice and
skips another object.
As you can see, there are two objects named 'var2' and no object named
'var1'. The c code is:
char *var1 = Hallo;
char *var2 = Hallo;
Zhiyi Zhang on 2015-05-27:
I have found the error report when I only used search==nurs:covnew as the
path search heuristic. It is
klee: ModuleUtil.cpp:435: llvm::Function*
klee::getDirectCallTarget(llvm::CallSite): Assertion `0 FIXME:
Unresolved
direct target for a constant
eric.ri...@huskers.unl.edu on 2015-05-30:
I'm not sure that what you are looking for exists. Klee is designed to test
programs and create test suites. It will find assertion violations and other
common errors. If you're looking to verify that a particular path through the
program is
Bin Lin on 2015-09-08:
Hello Martin,
Thank you!
After I set the LD_RUN_PATH, what command should I use in my case? If I use
the command './klee main.bc -load=path-to-lib/libfoo.so', I still get the
same error. So how to load the dynamic library in my case?
Try these, maybe one will work:
how so you just have one
bitcode file to give to KLEE.
On Tue, Sep 8, 2015 at 2:48 PM, Sean Bartell <s...@yotann.org> wrote:
Bin Lin on 2015-09-08:
Hello Martin,
Thank you!
After I set the LD_RUN_PATH, what command should I use in my case? If I
use the command './klee main.bc -load=path-
Riyad Parvez on 2015-09-23:
I was wondering whether it's possible mixed concrete-symbolic execution in
KLEE? Like S2E, where some of the input to the program will be symbolic and
other input will be concrete.
All inputs are concrete by default. You can make certain inputs symbolic by
either
RAJDEEP MUKHERJEE on 2016-06-23:
In default mode, klee uses dfs search strategy with incremental solving.
What additional optimisations does Klee perform with the --optimize switch ?
The --optimize switch causes KLEE to run standard compiler optimizations on the
subject program before
