Thank you very much!
------------------ ???????? ------------------
??????: "Xuzhijian"<[email protected]>;
????????: 2017??4??13??(??????) ????9:15
??????: "????"<[email protected]>; "klee-dev"<[email protected]>;
????: ????: [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
??????: [email protected]
[mailto:[email protected]] ???? ????
????????: 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.?6?7?6?7
?6?7#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; }
?6?7?6?7 when using klee to run it. there are three paths.?6?7
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'
?6?7 ?6?7 I understand "\x" is to ?6?7?6?7express hexadecimal number. then
what does the "}_9~" means in the red circle in the above picture ?
?6?7 ?6?7I would very much appreciate your help.?6?7_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
