Re: [klee-dev] [KLEE] write to a symbolic address & constraints for write

2020-11-24 Thread Cristian Cadar
Hi Mingyi, it's unclear to me what you are running exactly. In general, it's good to include a complete program and the exact commands you ran. Best wishes, Cristian On 20/11/2020 02:58, Liu, Mingyi wrote: Hi klee-dev members, I made args symbolic and provided a seed ktest file for the

[klee-dev] [KLEE] write to a symbolic address & constraints for write

2020-11-20 Thread Liu, Mingyi
Hi klee-dev members, I made args symbolic and provided a seed ktest file for the following target (code snippets): if (*(u64*)args >= 0x327b2000 && *(u64*)args <= 0x643c9000) { printf("WRITE\n"); *(u64*)*(u64*)args = 4; printf("val1 = %llx\n", *(u64*)args); printf("point_to1 = %p\n",