Question about --sym-argv

[李永超]

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.

[Sandeep Dasgupta]

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.

Post by 李永超
Hi,
I intended to feed symbolic program arguments to the .bc file using
#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
--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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev