[klee-dev] How to deterministic reproduce experimental results (instruction level) of default search strategy

Frank Busse f.busse17 at imperial.ac.uk
Fri Nov 30 16:49:44 GMT 2018


Hi,


On Thu, 29 Nov 2018 15:32:33 +0800
changze cui <changzecui at gmail.com> wrote:

>     For now, I am thinking there may be some other random number generator
> related to state selection which may influence instruction execution
> sequence.  But I haven't found it yet.

there are quite a few other sources for non-determinism, e.g.:

- environment variables
- number of files in your directory
- name of the executable
- other external concrete data (time stamps, ...)
- allocation scheme
- ...

If your traces diverge in the uclibc setup phase, this is most likely
the cause.  It might help to use -environ, -run-in,
-allocate-determ, ...


Good luck,

Frank



More information about the klee-dev mailing list