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
