[klee-dev] Sorry, may i ask a question?

[曾杰]

Hi,all
      I am very sorry to disturb you. Really thanks for the work Of Prof. Cristian Cadar. KLEE is one strong tool for testing softwares and symbolic execution is very promising. When i use klee to run the follow program, which is a similar example about the Vulnerability in the dissertation of Prof. Cristian Cadar for the degree of doctor of philosophy.

     the code of vulnerability existing in the function  safe_addptr in the 32-bit version of HISTAR kernel :
uintptr_t safe_addptr(int *of , uint64_t a, uint64_t b){
uintptr_t r=a+b;
if(r < a )
return r;
}

    i rewrite a similar program as bellow.​​
​#include<stdio.h> #include<malloc.h> #include <klee/klee.h> int main() {     unsigned long long int a;     unsigned long long int b;     unsigned int c;     klee_make_symbolic(&a,sizeof(a),"a");     klee_make_symbolic(&b,sizeof(b),"b");     c=a+b; if(c<a) { 	printf("yes \n"); } else if(c<b) { 	printf("xiaojie \n"); } else  	printf("no \n");     return 0; }


​​    when using klee to run it. there are three paths.​

    My question is about the generated test case which i cannot understand.



root at sucof-virtual-machine:~/桌面/xiaojiework/klee_work# ktest-tool ./klee-last/test000002.ktest
ktest file : './klee-last/test000002.ktest'
args       : ['overflowdetect_klee.bc']
num objects: 2
object    0: name: 'a'
object    0: size: 8
object    0: data: '\x01\x00FA\x00\x00\x00\x80'
object    1: name: 'b'
object    1: size: 8
object    1: data: '}_9~\x00\x00\x00\x00'



 ​  ​ I  understand "\x" is to ​​express hexadecimal number. then what does the "}_9~" means in the red circle in the above picture ?
​    ​I would very much appreciate your help.​
-------------- next part --------------
HTML attachment scrubbed and removed