[klee-dev] Symbolic Values Using Pointer and Struct
Jake Ekel
jakeekel at yahoo.com
Sun Dec 30 16:49:30 GMT 2018
Dear Sir/Madam,
Currently I am testing 2 programs using pointer and struct with KLEE. Below are the programs :
1st Program :
int len = 8;
int *a;
int main(){
a = malloc(len);
klee_make_symbolic(a, len, "a");
if(*a==10){
return 1;
}
return 0;
}
1st Program Test Result :ktest file : 'klee-last/test000001.ktest'
args : ['TestPointerKLEE.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 8
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00'
()
ktest file : 'klee-last/test000002.ktest'
args : ['TestPointerKLEE.bc']
num objects: 1
object 0: name: 'a'
object 0: size: 8
object 0: data: '\n\x00\x00\x00\xff\xff\xff\xff'
2nd Program :struct struct_value{
int int_value;
char char_value[10];
};
int main(){
struct struct_value sv;
klee_make_symbolic(&sv, sizeof(sv), "sv");
if(sv.int_value==10){
return 1;
}
if(sv.char_value=='a'){
return 2;
}
return 0;
}
2nd Program Test Result :ktest file : 'klee-last/test000001.ktest'
args : ['TestStructKLEE.bc']
num objects: 1
object 0: name: 'sv'
object 0: size: 16
object 0: data: '\n\x00\x00\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff'
()
ktest file : 'klee-last/test000002.ktest'
args : ['TestStructKLEE.bc']
num objects: 1
object 0: name: 'sv'
object 0: size: 16
object 0: data: '\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'
As we seen in the test result, the result for data are in hexadecimal format. May I know how to display the result for data in the normal format for pointer and struct? (for example if I put the KLEE symbolic values in the pointer of integer, the format result of data will be integer also).
Thank you.
Regards,Jake
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list