Skip to content

Commit c9956ec

Browse files
author
Viviane Garese
committed
Merge branch '133-xml-assertions' into 'master'
Fix reporting of assertion coverage Closes #133 See merge request eng/das/cov/gnatcoverage!320 Fix assertion level enabling, coverage obligation stats computing for ATCC, and adapt SCO kind image for better xml reporting Closes #133
2 parents 4ffdb5c + 0e3eb6a commit c9956ec

File tree

10 files changed

+291
-43
lines changed

10 files changed

+291
-43
lines changed

‎testsuite/tests/O212-062-xml/main.adb

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
pragma Ada_2012;
2+
pragma Assertion_Policy (Check);
3+
4+
procedure Main
5+
is
6+
function ATCC_Violation (X : Boolean) return Boolean
7+
with Pre => (X or else not X)
8+
is
9+
function Id (X : Boolean) return Boolean is
10+
begin
11+
if X or else X then
12+
return X;
13+
end if;
14+
return X;
15+
end Id;
16+
17+
Dummy : Boolean := Id (True);
18+
begin
19+
return Id (False);
20+
end ATCC_Violation;
21+
begin
22+
declare
23+
Dummy : Boolean := ATCC_Violation (True);
24+
begin
25+
null;
26+
end;
27+
return;
28+
end Main;

‎testsuite/tests/O212-062-xml/src-traces-index.xml.expected

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
<?xml version="1.0" ?>
2+
<document xmlns:xi="http://www.w3.org/2001/XInclude" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:noNamespaceSchemaLocation="gnatcov-xml-report.xsd">
3+
<coverage_report coverage_level="stmt+mcdc+atcc">
4+
<coverage_info>
5+
<xi:include parse="xml" href="trace.xml"/>
6+
</coverage_info>
7+
8+
<coverage_summary>
9+
<metric kind="total_lines_of_relevance" count="9"/>
10+
<metric kind="fully_covered" count="7" ratio="78"/>
11+
<metric kind="partially_covered" count="2" ratio="22"/>
12+
<metric kind="not_covered" count="0" ratio="0"/>
13+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
14+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
15+
<metric kind="exempted" count="0" ratio="0"/>
16+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
17+
<obligation_stats kind="Stmt">
18+
<metric kind="total_obligations_of_relevance" count="8"/>
19+
<metric kind="fully_covered" count="8" ratio="100"/>
20+
<metric kind="partially_covered" count="0" ratio="0"/>
21+
<metric kind="not_covered" count="0" ratio="0"/>
22+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
23+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
24+
<metric kind="exempted" count="0" ratio="0"/>
25+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
26+
</obligation_stats>
27+
28+
<obligation_stats kind="Decision">
29+
<metric kind="total_obligations_of_relevance" count="1"/>
30+
<metric kind="fully_covered" count="1" ratio="100"/>
31+
<metric kind="partially_covered" count="0" ratio="0"/>
32+
<metric kind="not_covered" count="0" ratio="0"/>
33+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
34+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
35+
<metric kind="exempted" count="0" ratio="0"/>
36+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
37+
</obligation_stats>
38+
39+
<obligation_stats kind="MCDC">
40+
<metric kind="total_obligations_of_relevance" count="2"/>
41+
<metric kind="fully_covered" count="1" ratio="50"/>
42+
<metric kind="partially_covered" count="0" ratio="0"/>
43+
<metric kind="not_covered" count="1" ratio="50"/>
44+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
45+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
46+
<metric kind="exempted" count="0" ratio="0"/>
47+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
48+
</obligation_stats>
49+
50+
<obligation_stats kind="ATC">
51+
<metric kind="total_obligations_of_relevance" count="1"/>
52+
<metric kind="fully_covered" count="1" ratio="100"/>
53+
<metric kind="partially_covered" count="0" ratio="0"/>
54+
<metric kind="not_covered" count="0" ratio="0"/>
55+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
56+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
57+
<metric kind="exempted" count="0" ratio="0"/>
58+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
59+
</obligation_stats>
60+
61+
<obligation_stats kind="ATCC">
62+
<metric kind="total_obligations_of_relevance" count="2"/>
63+
<metric kind="fully_covered" count="1" ratio="50"/>
64+
<metric kind="partially_covered" count="0" ratio="0"/>
65+
<metric kind="not_covered" count="1" ratio="50"/>
66+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
67+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
68+
<metric kind="exempted" count="0" ratio="0"/>
69+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
70+
</obligation_stats>
71+
72+
<file name="main.adb">
73+
<metric kind="total_lines_of_relevance" count="9"/>
74+
<metric kind="fully_covered" count="7" ratio="78"/>
75+
<metric kind="partially_covered" count="2" ratio="22"/>
76+
<metric kind="not_covered" count="0" ratio="0"/>
77+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
78+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
79+
<metric kind="exempted" count="0" ratio="0"/>
80+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
81+
<obligation_stats kind="Stmt">
82+
<metric kind="total_obligations_of_relevance" count="8"/>
83+
<metric kind="fully_covered" count="8" ratio="100"/>
84+
<metric kind="partially_covered" count="0" ratio="0"/>
85+
<metric kind="not_covered" count="0" ratio="0"/>
86+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
87+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
88+
<metric kind="exempted" count="0" ratio="0"/>
89+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
90+
</obligation_stats>
91+
92+
<obligation_stats kind="Decision">
93+
<metric kind="total_obligations_of_relevance" count="1"/>
94+
<metric kind="fully_covered" count="1" ratio="100"/>
95+
<metric kind="partially_covered" count="0" ratio="0"/>
96+
<metric kind="not_covered" count="0" ratio="0"/>
97+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
98+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
99+
<metric kind="exempted" count="0" ratio="0"/>
100+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
101+
</obligation_stats>
102+
103+
<obligation_stats kind="MCDC">
104+
<metric kind="total_obligations_of_relevance" count="2"/>
105+
<metric kind="fully_covered" count="1" ratio="50"/>
106+
<metric kind="partially_covered" count="0" ratio="0"/>
107+
<metric kind="not_covered" count="1" ratio="50"/>
108+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
109+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
110+
<metric kind="exempted" count="0" ratio="0"/>
111+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
112+
</obligation_stats>
113+
114+
<obligation_stats kind="ATC">
115+
<metric kind="total_obligations_of_relevance" count="1"/>
116+
<metric kind="fully_covered" count="1" ratio="100"/>
117+
<metric kind="partially_covered" count="0" ratio="0"/>
118+
<metric kind="not_covered" count="0" ratio="0"/>
119+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
120+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
121+
<metric kind="exempted" count="0" ratio="0"/>
122+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
123+
</obligation_stats>
124+
125+
<obligation_stats kind="ATCC">
126+
<metric kind="total_obligations_of_relevance" count="2"/>
127+
<metric kind="fully_covered" count="1" ratio="50"/>
128+
<metric kind="partially_covered" count="0" ratio="0"/>
129+
<metric kind="not_covered" count="1" ratio="50"/>
130+
<metric kind="undetermined_coverage" count="0" ratio="0"/>
131+
<metric kind="exempted_no_violation" count="0" ratio="0"/>
132+
<metric kind="exempted" count="0" ratio="0"/>
133+
<metric kind="exempted_undetermined_coverage" count="0" ratio="0"/>
134+
</obligation_stats>
135+
136+
</file>
137+
138+
</coverage_summary>
139+
140+
<sources>
141+
<xi:include parse="xml" href="main.adb.xml"/>
142+
</sources>
143+
144+
</coverage_report>
145+
146+
</document>
147+

‎testsuite/tests/O212-062-xml/test.opt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
bin-traces XFAIL Assertion coverage not yet supported for binary traces

‎testsuite/tests/O212-062-xml/test.py

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
"""
2+
Check the content of an XML summary for assertion coverage.
3+
"""
4+
5+
import os
6+
7+
from SCOV.minicheck import build_run_and_coverage
8+
from SUITE.cutils import Wdir
9+
from SUITE.gprutils import GPRswitches
10+
from SUITE.tutils import gprfor, thistest
11+
12+
wd = Wdir('tmp_')
13+
14+
gpr = gprfor(['main.adb'], srcdirs='..')
15+
xcov_args = build_run_and_coverage(
16+
gprsw=GPRswitches(root_project=gpr),
17+
covlevel='stmt+mcdc+atcc',
18+
mains=['main'],
19+
extra_coverage_args=['-axml'])
20+
21+
thistest.fail_if_diff(
22+
os.path.join("..", "src-traces-index.xml.expected"),
23+
os.path.join("obj", "index.xml")
24+
)
25+
26+
thistest.result()

‎tools/gnatcov/annotations-xml.ads

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,8 +34,8 @@ package Annotations.Xml is
3434
-- The following sections will describe each file type. The following
3535
-- convention will be used to denotate possible values for attributes:
3636
--
37-
-- * COVERAGE_KIND: can be either 'insn', 'branch', 'stmt',
38-
-- 'stmt+decision', 'stmt+mcdc'.
37+
-- * COVERAGE_KIND: can be either 'insn', 'branch', or one matching
38+
-- 'stmt(\+(decision|mcdc|uc_mcdc))?(\+(atc|atcc)?)?'
3939
-- * COVERAGE: can be either '+' (total coverage for the chosen coverage
4040
-- criteria), '-' (null coverage), '!' (partial coverage) or
4141
-- '.' (no code for this line).

‎tools/gnatcov/annotations.adb

Lines changed: 54 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1041,49 +1041,68 @@ package body Annotations is
10411041
Update_Level_Stats (SCO, Get_Line_State (SCO, Stmt), Stmt);
10421042
when Decision =>
10431043
if Coverage.Assertion_Coverage_Enabled
1044-
and then Decision_Type (SCO) in Pragma_Decision | Aspect
1044+
and then Is_Assertion (SCO)
10451045
then
10461046
Update_Level_Stats
10471047
(SCO, Get_Line_State (SCO, ATC), ATC);
10481048
else
10491049
Update_Level_Stats
10501050
(SCO, Get_Line_State (SCO, Decision), Decision);
1051+
end if;
1052+
1053+
declare
1054+
Assertion_Decision : constant Boolean :=
1055+
Coverage.Assertion_Condition_Coverage_Enabled
1056+
and then Is_Assertion (SCO);
1057+
begin
1058+
if Coverage.MCDC_Coverage_Enabled or else Assertion_Decision
1059+
then
1060+
declare
1061+
Condition_Level : constant Coverage_Level :=
1062+
(if Assertion_Decision
1063+
then Coverage.Assertion_Condition_Level
1064+
else Coverage.MCDC_Level);
1065+
begin
10511066

1052-
-- Conditions in that decision
1053-
1054-
if Coverage.MCDC_Coverage_Enabled then
1055-
for J in
1056-
Condition_Index'First .. Last_Cond_Index (SCO)
1057-
loop
1058-
declare
1059-
Condition_SCO : constant SCO_Id :=
1060-
Condition (SCO, J);
1061-
1062-
MCDC_State : constant SCO_State :=
1063-
Get_Line_State (SCO, MCDC);
1064-
-- If the parent decision is partially covered,
1065-
-- then the SCO_State for each condition will be
1066-
-- No_Code, and the SCO_State for the MCDC
1067-
-- Coverage_Level associated to the parent decision
1068-
-- SCO will be Not_Covered.
1069-
1070-
Condition_State : SCO_State;
1071-
1072-
begin
1073-
if MCDC_State = Not_Covered then
1074-
Condition_State := Not_Covered;
1075-
else
1076-
Condition_State :=
1077-
Get_Line_State
1078-
(Condition_SCO, Coverage.MCDC_Level);
1079-
end if;
1080-
1081-
Update_Level_Stats
1082-
(SCO, Condition_State, Coverage.MCDC_Level);
1083-
end;
1084-
end loop;
1067+
-- Conditions in that decision
1068+
1069+
for J in
1070+
Condition_Index'First .. Last_Cond_Index (SCO)
1071+
loop
1072+
declare
1073+
Condition_SCO : constant SCO_Id :=
1074+
Condition (SCO, J);
1075+
1076+
Line_Condition_State : constant SCO_State :=
1077+
Get_Line_State (SCO,
1078+
(if Assertion_Decision
1079+
then ATCC
1080+
else MCDC));
1081+
-- If the parent decision is partially covered,
1082+
-- then the SCO_State for each condition will be
1083+
-- No_Code, and the SCO_State for the
1084+
-- MCDC/Assertion condition Coverage_Level
1085+
-- associated to the parent decision SCO will be
1086+
-- Not_Covered.
1087+
1088+
Condition_State : SCO_State;
1089+
1090+
begin
1091+
if Line_Condition_State = Not_Covered then
1092+
Condition_State := Not_Covered;
1093+
else
1094+
Condition_State :=
1095+
Get_Line_State
1096+
(Condition_SCO, (Condition_Level));
1097+
end if;
1098+
1099+
Update_Level_Stats
1100+
(SCO, Condition_State, Condition_Level);
1101+
end;
1102+
end loop;
1103+
end;
10851104
end if;
1086-
end if;
1105+
end;
10871106
when others =>
10881107
null;
10891108
end case;

‎tools/gnatcov/coverage.adb

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,17 @@ package body Coverage is
128128
end if;
129129
end MCDC_Level;
130130

131+
-------------------------------
132+
-- Assertion_Condition_Level --
133+
-------------------------------
134+
135+
function Assertion_Condition_Level return Contract_Condition_Level is
136+
begin
137+
pragma Assert (Assertion_Condition_Coverage_Enabled);
138+
pragma Assert (Enabled (ATCC));
139+
return ATCC;
140+
end Assertion_Condition_Level;
141+
131142
----------------
132143
-- Object_Level --
133144
----------------
@@ -208,7 +219,7 @@ package body Coverage is
208219
Res.Include (MCDC_Level);
209220
end if;
210221
end if;
211-
if Enabled (ATC) then
222+
if Assertion_Coverage_Enabled then
212223
Res.Include (ATC);
213224
if Enabled (ATCC) then
214225
Res.Include (ATCC);

‎tools/gnatcov/coverage.ads

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,9 +74,12 @@ package Coverage is
7474
-- one is enabled (it is illegal to have both enabled).
7575

7676
function MCDC_Level return MCDC_Coverage_Level;
77-
-- If MCDC_Coverage_Level_Enabled, return MCDC or UC_MCDC, depending on
77+
-- If MCDC_Coverage_Enabled, return MCDC or UC_MCDC, depending on
7878
-- which one is enabled (it is illegal to have both enabled).
7979

80+
function Assertion_Condition_Level return Contract_Condition_Level;
81+
-- If Assertion_Condition_Coverage_Enabled, return ATCC.
82+
8083
function Coverage_Option_Value return String;
8184
-- Return the coverage option value for the currently enabled levels
8285

‎tools/gnatcov/coverage_options.ads

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,9 +51,10 @@ package Coverage_Options is
5151
-- least once as part of an evaluation to True of the whole
5252
-- decision.
5353

54-
subtype Object_Coverage_Level is Coverage_Level range Insn .. Branch;
55-
subtype Source_Coverage_Level is Coverage_Level range Stmt .. ATCC;
56-
subtype MCDC_Coverage_Level is Coverage_Level range MCDC .. UC_MCDC;
54+
subtype Object_Coverage_Level is Coverage_Level range Insn .. Branch;
55+
subtype Source_Coverage_Level is Coverage_Level range Stmt .. ATCC;
56+
subtype MCDC_Coverage_Level is Coverage_Level range MCDC .. UC_MCDC;
57+
subtype Contract_Condition_Level is Coverage_Level range ATCC .. ATCC;
5758

5859
type Levels_Type is array (Coverage_Level) of Boolean;
5960
-- Set of Coverage_Levels

‎tools/gnatcov/sc_obligations.adb

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2741,9 +2741,21 @@ package body SC_Obligations is
27412741
return "<no SCO>";
27422742
else
27432743
declare
2744-
SCOD : constant SCO_Descriptor := SCO_Vector (SCO);
2744+
SCOD : SCO_Descriptor renames SCO_Vector.Reference (SCO);
2745+
From_Assertion : constant Boolean := Assertion_Coverage_Enabled
2746+
and then
2747+
((SCOD.Kind = Decision
2748+
and then SCOD.D_Kind in Pragma_Decision | Aspect)
2749+
or else
2750+
(SCOD.Kind = Condition
2751+
and then SCO_Vector.Reference
2752+
(Enclosing_Decision (SCO)).D_Kind in
2753+
Pragma_Decision | Aspect));
27452754
begin
27462755
return "SCO #" & Trim (SCO'Img, Side => Ada.Strings.Both) & ": "
2756+
& (if From_Assertion
2757+
then "ASSERTION "
2758+
else "")
27472759
& SCO_Kind'Image (SCOD.Kind)
27482760
& Op_Kind_Image
27492761
& Sloc_Image (SCOD.Sloc_Range);

0 commit comments

Comments
 (0)