Hello Sir,
My name is Wei-Fan, and I am currently a graduate student at University
of Utah.
I currently tried to build KLEE with some other external libraries.
I tried to configure KLEE by:
./configure --libs=-lgmp -lmpfr
of
./configure --with-libs=-lgmp -lmpfr
But they didn't
Hi Lei,
Thank you for your detailed instruction. Now we do like that. And,
another question, I think there are actually only 88 stand-alone
utilities in coreutils, unless considering false or test/[ as
stand-alone. I skipped dir, vdir, ginstall, groups, sha*sum,
false, and only test one of the
Hi Yi,
We used this sequence:
mkdir obj-klee
make -w O=obj-klee defconfig
cd obj-klee
make CC=klee-gcc LD=llvm-ld --disable-opt AR=llvm-ar SKIP_STRIP=y V=1
ln -s busybox_unstripped.bc toolname (for each tool you want to run)
You might need to adjust this a bit (I noticed that on my current
I want to work with examples that has float. Can KLEE deal with this?
KLEE cannot currently handle symbolic floating point expressions. A
fork KLEE called KLEE-FP can handle symbolic floating point
expressions. See http://www.pcc.me.uk/~peter/klee-fp/
Just a quick clarification: KLEE-FP has
Hi Cristian,
Thanks so much.
YI and Yi: please try it and redo your experiments.
Jian LIU
email to: gjk@gmail.com
2013/3/7 Cristian Cadar c.ca...@imperial.ac.uk
Hi Yi,
We used this sequence:
mkdir obj-klee
make -w O=obj-klee defconfig
cd obj-klee
make
Hello.
Yes.
So KLEE takes into account only the coverage, if all paths are covered, but
does not take into account entire design structure.
The errors provided by siemens benchmarks are in the operators (+ - -, - ,
etc) and in numbers (2 - 3, 70 - 80), and with klee inputs even if
At one time I was playing around with KLEE. The goal was to see if MCDC
coverage was possible.
It was not.
By coincidence I discovered CIL a C language program transformation tool.
Try
(1) transform the source using CIL
(2) generate test cases using KLEE operating upon the transformed source
(3)
