[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