If the character is visible, then klee will show it directly, otherwise, it will show it as a hexadecimal number, so I think “}_9~\x00\x00\x00\x00”, means “\x7d\x5f\x39\x7e\x00\x00\x00\x00” in hexadecimal
发件人: klee-dev-boun...@imperial.ac.uk [mailto:klee-dev-boun...@imperial.ac.uk] 代表 曾杰 发送时间: 2017年4月12日 10:22 收件人: klee-dev 主题: [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@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.
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
