Feature #10974
closed
Parse and merge debug data presented by CPAchecker
Added by Evgeny Novikov about 3 years ago.
Updated almost 3 years ago.
Category:
Results processing
Description
CPAchecker provides such debug data as values of variables and time spent for executing stop operator. They are shown well for code coverage of verification tasks, but then it is not merged and presented for total code coverage. To merge it we will have to parse it in advance, that means that data should have a specific format.
- Status changed from New to Resolved
I did this in branch "merge-smg-debug-info" that is tested right now.
- Status changed from Resolved to Closed
Tests passed, so I merged the branch to master in 57efbed80.
BTW, this is fairly important for decomposition of environment models, since there may be many verification tasks for the same pair of a module and a requirements specification. Different verification tasks can have different code coverage for the same source code locations. Before it was overwritten while now it is merged properly.
Also available in: Atom
PDF