Hi,
I observed that when asked for a counterexample, kleaver picks the smallest
valid value. I’m wondering if there’s a way to “seed the solver” so that it
prioritizes the value given in the seed? For example, given constraint x != 1,
the counterexample value would be 0. With a seed value 3,
Hi,
I’m wondering whether klee generate constraints when a concrete value is
written to symbolic position? I tried a toy program and it seemed klee doesn’t.
Specifically, I added a `buf[1] = ‘9’ before the password check in
check_password(). But I only get constraint: (Eq 104 (Read w8 0
be symbolic.
Best,
Weiqi
From: Weiqi Wang<mailto:wq.w...@mail.utoronto.ca>
Sent: Friday, August 20, 2021 6:55 PM
To: klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk>
Subject: [klee-dev] About filename extension of symbolic files
EXTERNAL EMAIL:
Hi,
I was trying to run klee with Graph
Hi,
I was trying to run klee with GraphicsMagick(GM) using command:
klee --disable-verify --only-replay-seeds --libc=uclibc --posix-runtime
--seed-file rectangular.ktest ./gm.bc identify A -sym-files 1 80
rectangular.ktest is generated using `gen-bout –sym-file rectangular.mvg
–but-file
ename length for kleaver
EXTERNAL EMAIL:
Hi Weiqi,
I haven't looked at the code yet, but if this happens only for filenames
longer than 32 characters, this might be a bug. Can you file an issue
on GitHub, with an example?
Best,
Cristian
On 06/08/2021 21:23, Weiqi Wang wrote:
> Hi
Hi,
I noticed that kleaver generates different solutions if the .kquery filename is
longer than 32 characters. Is the filename used as some kind of seed for the
solver?
Best,
Weiqi
___
klee-dev mailing list
klee-dev@imperial.ac.uk
