Feature request for 'min/max stack depth option'


I know there is an option to limit the maximum number of ExplodedNode’s, in case the symbolic execution path is getting out of the hands. I tried to increase the limit so that the analyzer can reflect the error context (i.e., stack frame) better, but I turns out this option not necessarily guarantees the extended stack frame context, while the analysis time gets severely delayed.

What I want to propose here is that, instead of arbitrary limiting the number of nodes, limiting the minimum and maximum stack depth of a certain path could enable more accurate analysis (in terms of its error ‘context’), while still restricting its resource consumption (including time).

I suppose this is not at all a simple idea (as the error context is unknown before stumbling upon an error while the stack depth is widely varying), I post it here just so that anyone having any idea can propose something when he/she reads this and thinks it’s a neat idea.

Thank you,
Gwangmu Lee.