[klee-dev] deterministic memory in KLEE

[Oleg Sokolsky]

Dear KLEE community,

I have a program that, after a long run in KLEE, runs out of 
deterministic memory.  To the best of my knowledge, it does not allocate 
dynamic objects.  But it does make a lot of non-recursive function calls.

Our suspicion currently is that KLEE allocates memory objects for 
function parameters and local variables and, after the function returns, 
they stay in the deterministic memory until it is eventually exhausted.  
Does this suspicion sound right and, if so, is there a way around it.  
And, otherwise, what could be the reason?

Thanks,
Oleg