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

Re: [klee-dev] How to make assumption on symbolic stdin in klee

2020-11-24 Thread Cristian Cadar
Hi Pushi, to do this, you will need to modify the code in runtime/POSIX. Best, Cristian On 16/11/2020 12:34, Pushi Zhang wrote: Hi all,       As in the documentation of klee, we can use command "-sym-stdin" to make inputs symbolic.       Here my question is: how can we make assumptions

Re: [klee-dev] KLEE floating-point support

2020-11-24 Thread Cristian Cadar
Hi Aleksei, From what I understand, you managed to rebase the KLEE-Float extension on top of KLEE's mainline. That's great! As I mentioned on GitHub, my main concern is that KLEE-Float changes the expression representation, which has a significant impact on the core of KLEE. The question