[klee-dev] Stack overflow within STP
sbkim at stanford.edu
Wed Oct 28 19:01:07 PDT 2009
You're right. I've been using --use-forked-stp all the time, but
it turns out that --with-stp-server switches the base solver from
STPSolver to STPServerSolver, which doesn't respect --use-forked-stp.
Making STPServerSolver respect the option and forking seems to be
the best solution.
Dawson Engler wrote:
> Maybe I'm misunderstanding something --- can't you just run STP as a
> forked process? That seems like it would solve your issue.
>> I have been encountering stack overflow in STP, which is caused by
>> function calls more than 6000 levels deep. The functions include
>> BEEV::ASTNode::LetizeNode and BEEV::BeevMgr::TermToConstTermUsingModel,
>> calling themselves, respectively.
>> At least in one case I observed that it was not a bug in the logic
>> but a very complex query that could be causing the problem.
>> The stack overflow manifests itself in the form of segmentation faults,
>> which I cannot "catch" in the program like a C++ exception. When this
>> happens, everything stops and I lose valuable states that have not
>> finished and produced test cases. I could use a signal handler, but
>> that would handle all segfaults, and I'm not sure if it's a good idea.
>> Do you have any good ideas?
More information about the klee-dev