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

[曾杰]

Thank you very much! 




------------------ 原始邮件 ------------------
发件人: "Xuzhijian"<xuzhijian at huawei.com>; 
发送时间: 2017年4月13日(星期四) 上午9:15
收件人: "曾杰"<zyj183247166 at qq.com>; "klee-dev"<klee-dev at imperial.ac.uk>; 
主题: 答复: [klee-dev] Sorry, may i ask a question?



 
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