[klee-dev] Question about --sym-argv

[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.


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
> klee-dev at imperial.ac.uk
> 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
-------------- next part --------------
HTML attachment scrubbed and removed