Remove summary edges
Original issue created by @PhilippWendler on 2014-12-16 at 11:26:36, last modified on 2014-12-16 at 11:26:36
If -skipRecursion
is enabled, we currently insert additional CFunctionSummaryStatementEdge
s for skipping recursive function calls into the CFA (with the option analysis.summaryEdges=true
).
Modifying the CFA in this way is a problem, because we cannot use the same CFA for multiple analyses when some want to skip recursion and some do not.
Furthermore, this leads to two edges that connect the same locations (the edge mentioned above and the classic summary edge), and these edges compare as equal.
As discussed below, the cleanest way is to get rid of the summary edges and just keep the regular CFunctionSummaryStatementEdge
for connecting the call node and return node of a function call.
This can be done with the following steps:
- Test
analysis.summaryEdges=true
more extensively (not only SV-COMP configuration with-benchmark
but also for other configs and with assertions and output files enabled). - Hard-code
analysis.summaryEdges=true
. - Move code away from using summary edges. Often these edges are just used to get some specific information like the call node or the
CFunctionCall
object, in which case this is easy. In other cases, theCFunctionSummaryStatementEdge
could be used instead. - Remove summary edges once completely unused.