Hi all,
I'm generating the .smt2 file for the following simple c program:
#include <klee/klee.h>
int main() {
int a;
int another;
klee_make_symbolic(&a, sizeof(a), "a");
klee_make_symbolic(&another, sizeof(another), "another");
if ( a == 77 ) {
a += 6;
another = 5;
} else {
a = 9;
if ( another == 12 ) {
a += 7;
} else {
a += 10;
}
}
return 0;
}
I can compile it using clang -I ../../include -emit-llvm -c -g simple.c and
obtain the .smt2 running klee -write-smt2s simple.bc. At this point I would
like to see the model for the 3 test case and I have the following results:
klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test000001.ktest
ktest file : 'klee-last/test000001.ktest'
args : ['simple.bc']
num objects: 2
object 0: name: b'a'
object 0: size: 4
object 0: data: 77
object 1: name: b'another'
object 1: size: 4
object 1: data: 0
klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test000002.ktest
ktest file : 'klee-last/test000002.ktest'
args : ['simple.bc']
num objects: 2
object 0: name: b'a'
object 0: size: 4
object 0: data: 0
object 1: name: b'another'
object 1: size: 4
object 1: data: 0
klee@a8a6399e6799:~/klee_src/examples/simple$ ktest-tool --write-ints
klee-last/test000003.ktest
ktest file : 'klee-last/test000003.ktest'
args : ['simple.bc']
num objects: 2
object 0: name: b'a'
object 0: size: 4
object 0: data: 0
object 1: name: b'another'
object 1: size: 4
object 1: data: 12
I feel I'm missing something because, for instance, I cannot see the case
where a = 0 and another = 12.
Can you help me to understand if the models are correct and why?
Thanks
Alberto
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
