why different traces are generated under the same input?

[Qiuping Yi]

Hi,

I ran klee on 'findutils' under the same input without any symbolic
variable, and want to get a determinate execution. However, I get two
different executions randomly(one path with a bigger probability). Why?
How can I get a determinate execution? Thank you very much.


--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences

[Cristian Cadar]

Hi Qiuping,

Can you open an issue on GitHub where you provide more details
(including the LLVM bitcode file that you are running)? The way I would
suggest to start debugging this is to look where the two paths diverge,
and first check whether there is any non-determinism in the program itself.

Best,
Cristian

Post by Qiuping Yi
Hi,
I ran klee on 'findutils' under the same input without any symbolic
variable, and want to get a determinate execution. However, I get two
different executions randomly(one path with a bigger probability). Why?
How can I get a determinate execution? Thank you very much.
--------------------------------------------
Qiuping Yi
Institute Of Software
Chinese Academy of Sciences
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev