On 27 March 2018 at 08:45, Sicco Verwer <s.e.ver...@tudelft.nl> wrote: > > Dear all, > > I am trying to run KLEE in my class on concolic execution. Some student get > the following message after which KLEE quits, and I cannot seem to find the > cause, or solution. Does anyone know?
Just to be explicitly clear. KLEE does not use concolic execution. KLEE implements classical symbolic execution where by it stores every path (and related state) in memory at the same time. This gives KLEE a global view of feasible paths in the programs but this approach can quickly lead to memory exhaustion. The issues you're seeing points at memory exhaustion which is one of the limitations of classical symbolic execution. Concolic execution side steps this by not storing the execution state of every path it discovers. You could try using the Z3 solver instead of STP if you want to avoid forking which might reduce some of the memory overhead. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
