Can you please try:
klee -libc=uclibc -posix-runtime ./src.bc -sym-arg 2
as per klee help-posix-runtime
with POSIX runtime. Options that can be passed as *arguments to the
programs* are: --sym-argv <max-len> --sym-argvs <min-argvs> <max-argvs>
<max-len> + file model options
But I found that with different values n for -*sym-arg n*, I am getting
(n+1) testcases. I do not understand why.
On 01/14/2014 08:42 PM, ??? wrote:
Hi,
I intended to feed symbolic program arguments to the .bc file using
--sym-argvs. The source code is:
#include <stdio.h>
#include <string.h>
int main(int argc, char * argv[]) {
char buf[10];
char buf_2[10];
int i = 1;
printf("%s", argv[1]);
if(argv[1][0] == 'l')
strcpy(buf, argv[1]);
else
buf[i] = 'l';
return 0;
}
My command invoking KLEE is: klee ./src.bc --libc=uclibc
-posix-runtime --sym-argv 2.
However, after KLEE finishing the execution, only 1 path is covered
and the output of KLEE is:
--libc=uclibc
KLEE: done: total instructions = 33
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
indicating that argv[1] is actually the argument I exactly used in the
command line(--libc=uclibc) rather than symbolic values.
Could anyone point out the cause of my problem?
Thanks,
Yongchao.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
University Of Illinois Urbana Champaign
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
