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

[Xuzhijian]

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-bounces at imperial.ac.uk [mailto:klee-dev-bounces at 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 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