[klee-dev] why different traces are generated under the same input?

Cristian Cadar c.cadar at imperial.ac.uk
Mon Nov 4 10:57:29 GMT 2013


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

On 02/11/13 16:20, Qiuping Yi wrote:
> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>




More information about the klee-dev mailing list