Project

General

Profile

Actions
Copy link

Feature #10974

closed

Parse and merge debug data presented by CPAchecker

Added by Evgeny Novikov about 3 years ago. Updated almost 3 years ago.

Status:
Closed
Priority:
High
Assignee:
Evgeny Novikov
Category:
Results processing
Target version:
3.4
Start date:
10/07/2021
Due date:
% Done:

0%

Estimated time:
Published in build:

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.

Actions
Copy link
 #1

Updated by Evgeny Novikov almost 3 years ago

  • Status changed from New to Resolved

I did this in branch "merge-smg-debug-info" that is tested right now.

Actions
Copy link
 #2

Updated by Evgeny Novikov almost 3 years ago

  • 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.

Actions
Copy link

Also available in: Atom PDF