Skip to content

Commit 0e3eb6a

Browse files
author
Viviane Garèse
committed
Fix assertion coverage reporting
Fix assertion level enabling, coverage obligation stats computing for ATCC, and adapt SCO kind image for better xml reporting
1 parent 4ffdb5c commit 0e3eb6a

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)