Hello Urmas,
It's not that clear what you're trying to do but I assume you want to use the
inputs generated by KLEE on one program version to test 41 variants. I'm afraid
this might not be that easy.
KLEE actually gets nearly 100% statement and branch coverage on the original
program ('nearly' because there's some unreachable code). You should run it
without the POSIX runtime and uclibc because you're not using them anyway. What
you get is:
--------------------------------------------------------------------------
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount | Solver(%) |
--------------------------------------------------------------------------
| klee-out-0 | 5951 | 0.26 | 99.36 | 94.44 | 311 | 91.92 |
--------------------------------------------------------------------------
From what I can tell, the path coverage is also 100%, counting just feasible
paths, so there are no other inputs to generate as far as KLEE is concerned.
Paul
On 6 Mar 2013, at 12:31, Urmas Repinski <[email protected]> wrote:
> Hello.
>
> My name is Urmas Repinski, PhD student in Tallinn University of Technology,
> Estonia.
>
> I am trying to generate inputs for Siemens Benchmarks with KLEE.
>
> Siemens Benchmarks - C designs with various erroneous versions for testing
> error localization and error correction in C designs.
> They can be located and downloaded from
> http://pleuma.cc.gatech.edu/aristotle/Tools/subjects/
>
> I am testing KLEE with tcas design, it is smallest and simplest.
>
> Siemens benchmarks provide their inputs, tcas/script/runall.sh script has
> 1607 lines of execution of the design, and it is easy extract 1607 various
> inputs for the design.
> But i have no idea how the inputs were generated, attaching siemens
> benchmarks inputs to the letter (file INPUTS_tcas_Siemens_arg).
>
> I want to compare Siemens inputs with inputs, generated by klee.
>
> I had installed klee as it is written in documentation -
> http://klee.llvm.org/GetStarted.html - with uclibc support.
>
> Installed llvm-gcc-4.2, llvm-gcc-4.5, originally provided by Linux Mint 12
> uses too new version of gcc, and this generated error then used llvm-gcc, but
> ok, this error solved.
>
> When i take tcas/v1/tcas.c design, adding corresponding modification to
> generate inputs with klee (tcas_original.c and tcas_modified.c are attached
> to the letter), i get 45 inputs generated, and after modifying klee output to
> suitable format i get klee outputs (file KLEE_OUTPUT_arg).
>
> urmas-PBL21 src # llvm-gcc --emit-llvm -c -g tcas.c
> urmas-PBL21 src # klee --libc=uclibc --posix-runtime tcas.o
> KLEE: NOTE: Using model:
> /home/urmas/forensic/thirdparty-install/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
> KLEE: output directory = "klee-out-143"
> KLEE: WARNING: undefined reference to function: fwrite
> KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 54549392)
> KLEE: WARNING ONCE: calling __user_main with extra arguments.
>
> KLEE: done: total instructions = 14790
> KLEE: done: completed paths = 45
> KLEE: done: generated tests = 45
>
>
> This outputs have same coverage than Siemens Inputs, but most of errors in
> erroneous designs are simply not detected, while Simenes inputs detect all
> errors.
>
> Inputs KLEE: Coverage - 92.5532%. Total Inputs - 45 Detected Errors - 8/41
> Inputs Siemens Benchmarks: Coverage - 93.0851%. Total Inputs - 1607, Detected
> Erroneous designs - 41/41
>
> Maybe i have something wrong with KLEE arguments when i execute klee, can
> somebody help me with right klee execution?
> I had tested klee with various options, but i still have 45 generated inputs.
> Is it possible to increase somehow number of generated inputs with klee?
> Maybe WARNING KLEE: WARNING: undefined reference to function: fwrite aborts
> executions somewhere, but there is no fwrite function in tcas design.
>
> Urmas Repinski
> <INPUTS_tcas_Siemens_arg><tcas_original.c><tcas_modified.c><KLEE_OUTPUT_arg>_______________________________________________
> klee-dev mailing list
> [email protected]
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
