Hello
I have a simple question, I hope someone can help me.
I want analyze the paths after the assignment a=3
I thought that it could be with --make-concret-symbolic
but I didn't obtain the result that I thought.
¿Is there some way to obtain all the paths ?¿even if we give value to a
variable after we make it symbolic?
For the next simplex I want have a=10 and a!=10
Thanks very much
Regards
I have next example:
______________________
int main() {
int a;
* klee_make_symbolic(&a, sizeof(a), "a");
a=10;*
if(a == 10)printf("a= 10");
else printf("a !=10");
return 0;
}
_______________________
*Results*
>klee --make-concrete-symbolic=1 concretevalues.o
KLEE: output directory = "klee-out-39"
KLEE: WARNING: undefined reference to function: printf
Making symbolic: (NotOptimized (Eq 10
(ReadLSB w32 0 rrws_arr1)))
KLEE: WARNING: calling external: printf(155069800)
a==10Making symbolic: (NotOptimized (Eq 0
(ReadLSB w32 0 rrws_arr2)))
KLEE: done: total instructions = 18
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
:
>ktest-tool --write-ints klee-last/*.ktest
ktest file : 'klee-last/test000001.ktest'
args : ['concretevalues.o']
num objects: 1
object 0: name: 'a'
object 0: size: 4
object 0: data: 0
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
