Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 2639a54

Browse files
RenjiSannRenjiSann
committedDec 3, 2024
Add gexpr coverage level
1 parent 2dd5b8d commit 2639a54

13 files changed

+286
-43
lines changed
 

Diff for: ‎tools/gnatcov/annotations-sarif.adb

+9
Original file line numberDiff line numberDiff line change
@@ -203,6 +203,15 @@ package body Annotations.Sarif is
203203
& "gnatcov/cov_source.html#function-and-call-coverage-fun-call-"
204204
& "analysis-experimental",
205205
Config => +"error"),
206+
Source_Coverage_Level'Pos (GExpr) =>
207+
(Id => +GExpr'Image,
208+
Name => +"Guarded Expression coverage",
209+
Short_Descr =>
210+
(+"The expression belongs to a conditional expression structure"
211+
& " and was executed at least once"),
212+
Help_Uri => +Doc_Link
213+
& "gnatcov/cov_source.html#foobar", -- FIXME(dprn): valid URL
214+
Config => +"error"),
206215
Undet_Rule =>
207216
(Id => +"UNDET",
208217
Name => +"Undetermined Coverage",

Diff for: ‎tools/gnatcov/annotations.adb

+8
Original file line numberDiff line numberDiff line change
@@ -388,6 +388,11 @@ package body Annotations is
388388
Pretty_Print_Call (Pp, SCO, SCO_State);
389389
end if;
390390

391+
when Guarded_Expr =>
392+
if Coverage.Enabled (GExpr) then
393+
SCO_State := Get_Line_State (SCO, GExpr);
394+
Pretty_Print_Statement (Pp, SCO, SCO_State);
395+
end if;
391396
end case;
392397
end if;
393398
end loop;
@@ -1245,6 +1250,9 @@ package body Annotations is
12451250
when Fun_Call_SCO_Kind =>
12461251
return Coverage_Level'Pos (Fun_Call);
12471252

1253+
when Guarded_Expr =>
1254+
return Coverage_Level'Pos (GExpr);
1255+
12481256
when others =>
12491257
return Other_Errors;
12501258
end case;

Diff for: ‎tools/gnatcov/checkpoints.adb

+4-3
Original file line numberDiff line numberDiff line change
@@ -503,7 +503,7 @@ package body Checkpoints is
503503
Supported_Levels (MCDC_Coverage_Level'Range) := (others => True);
504504
Supported_Levels (Decision) := True;
505505
end if;
506-
for Level in Insn .. Fun_Call loop
506+
for Level in Insn .. GExpr loop
507507
CSS.Write (Supported_Levels (Level));
508508
end loop;
509509

@@ -641,7 +641,7 @@ package body Checkpoints is
641641
-- reading code.
642642

643643
declare
644-
CP_Levels : U8_Array (1 .. 9);
644+
CP_Levels : U8_Array (1 .. 10);
645645
Levels : Levels_Type;
646646
begin
647647
CLS.Read (CP_Levels);
@@ -654,7 +654,8 @@ package body Checkpoints is
654654
UC_MCDC => Boolean'Val (CP_Levels (6)),
655655
ATC => Boolean'Val (CP_Levels (7)),
656656
ATCC => Boolean'Val (CP_Levels (8)),
657-
Fun_Call => Boolean'Val (CP_Levels (9)));
657+
Fun_Call => Boolean'Val (CP_Levels (9)),
658+
GExpr => Boolean'Val (CP_Levels (10)));
658659
declare
659660
Error_Msg : constant String :=
660661
Coverage.Is_Load_Allowed (Filename, Levels);

Diff for: ‎tools/gnatcov/checkpoints.ads

+2-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ with Traces_Source; use Traces_Source;
3939

4040
package Checkpoints is
4141

42-
subtype Checkpoint_Version is Interfaces.Unsigned_32 range 1 .. 16;
42+
subtype Checkpoint_Version is Interfaces.Unsigned_32 range 1 .. 17;
4343
-- For compatibility with previous Gnatcov versions, the checkpoint
4444
-- file format is versioned.
4545
--
@@ -60,6 +60,7 @@ package Checkpoints is
6060
-- 14 -- Extend CU_Info to implement block coverage
6161
-- 15 -- Increase size of Pragma_Id after addition of 255th pragma
6262
-- 16 -- Extend Scope_Entity to include the Start/End_Sloc of the scope
63+
-- 17 -- Add support for Fun_Call and Guarded Expression coverage
6364
--
6465
-- Note that we always use the last version when creating a checkpoint.
6566
--

Diff for: ‎tools/gnatcov/coverage-source.adb

+34-3
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,11 @@ package body Coverage.Source is
129129

130130
when Fun_Call_SCO_Kind =>
131131
Fun_Call_Executed : Boolean := False;
132-
-- Set to True id this call or function was executed at least once
132+
-- Set to True if this call or function was executed at least once
133+
134+
when Guarded_Expr =>
135+
GExpr_Executed : Boolean := False;
136+
-- Set to True if this was executed at least once
133137

134138
when others =>
135139
null;
@@ -1179,6 +1183,24 @@ package body Coverage.Source is
11791183
SCO_State := SCI.State (Fun_Call);
11801184
Update_Line_State
11811185
(Line_Info, SCO, SCI.Tag, Fun_Call, SCO_State);
1186+
elsif Kind (SCO) = Guarded_Expr
1187+
and then Enabled (GExpr)
1188+
then
1189+
if SCI.GExpr_Executed then
1190+
SCO_State := Covered;
1191+
else
1192+
SCO_State := Not_Covered;
1193+
1194+
-- Report a violation on the first line of the SCO to
1195+
-- avoid duplicating violations in the report.
1196+
1197+
if Line_Num = First_Sloc (SCO).L.Line then
1198+
Report_Violation (SCO, SCI.Tag, "not executed");
1199+
end if;
1200+
end if;
1201+
1202+
Update_Line_State
1203+
(Line_Info, SCO, SCI.Tag, GExpr, SCO_State);
11821204
end if;
11831205
end loop;
11841206
end SCOs_Of_Line;
@@ -2142,6 +2164,8 @@ package body Coverage.Source is
21422164
SCI.Executed := True;
21432165
elsif SCI.Kind in Fun_Call_SCO_Kind then
21442166
SCI.Fun_Call_Executed := True;
2167+
elsif SCI.Kind = Guarded_Expr then
2168+
SCI.GExpr_Executed := True;
21452169
end if;
21462170

21472171
end Set_Executed;
@@ -2596,7 +2620,7 @@ package body Coverage.Source is
25962620

25972621
-- Skip bits corresponding to fun_call obligations
25982622

2599-
if Kind (Stmt_Bit_Map (Bit)) in Fun_Call_SCO_Kind then
2623+
if Kind (Stmt_Bit_Map (Bit)) /= Statement then
26002624
goto Continue;
26012625
end if;
26022626

@@ -2707,7 +2731,7 @@ package body Coverage.Source is
27072731
CP_SCI.Tag := SC_Tag (CLS.Read_I32);
27082732

27092733
declare
2710-
States : array (1 .. 9) of Line_State;
2734+
States : array (1 .. 10) of Line_State;
27112735
begin
27122736
for I in States'Range loop
27132737
States (I) := CLS.Read_Line_State;
@@ -2721,6 +2745,7 @@ package body Coverage.Source is
27212745
CP_SCI.State (ATC) := States (7);
27222746
CP_SCI.State (ATCC) := States (8);
27232747
CP_SCI.State (Fun_Call) := States (9);
2748+
CP_SCI.State (GExpr) := States (10);
27242749
end;
27252750

27262751
case CP_SCI.Kind is
@@ -2740,6 +2765,9 @@ package body Coverage.Source is
27402765
when Fun_Call_SCO_Kind =>
27412766
CP_SCI.Fun_Call_Executed := CLS.Read_Boolean;
27422767

2768+
when Guarded_Expr =>
2769+
CP_SCI.GExpr_Executed := CLS.Read_Boolean;
2770+
27432771
when others =>
27442772
null;
27452773
end case;
@@ -2783,6 +2811,9 @@ package body Coverage.Source is
27832811
when Fun_Call_SCO_Kind =>
27842812
CSS.Write (Value.Fun_Call_Executed);
27852813

2814+
when Guarded_Expr =>
2815+
CSS.Write (Value.GExpr_Executed);
2816+
27862817
when others =>
27872818
null;
27882819
end case;

Diff for: ‎tools/gnatcov/coverage.adb

+3
Original file line numberDiff line numberDiff line change
@@ -226,6 +226,9 @@ package body Coverage is
226226
if Enabled (Fun_Call) then
227227
Res.Include (Fun_Call);
228228
end if;
229+
if Enabled (GExpr) then
230+
Res.Include (GExpr);
231+
end if;
229232
end if;
230233
return Res;
231234
end Source_Levels_Enabled;

Diff for: ‎tools/gnatcov/coverage.ads

+2-1
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,8 @@ package Coverage is
4343
when UC_MCDC => "UC_MCDC",
4444
when ATC => "ATC",
4545
when ATCC => "ATCC",
46-
when Fun_Call => "Function and call");
46+
when Fun_Call => "Function and call",
47+
when GExpr => "Guarded expression");
4748
-- Case sensitive version of Coverage_Level'Image
4849

4950
procedure Set_Coverage_Levels (Opt : String);

Diff for: ‎tools/gnatcov/coverage_options.adb

+23-1
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,8 @@ package body Coverage_Options is
133133
& "+" & Level_Str (UC_MCDC) & ")?"
134134
& "(+" & Level_Str (ATC) & "|"
135135
& "+" & Level_Str (ATCC) & ")?"
136-
& "(+" & Level_Str (Fun_Call) & ")?";
136+
& "(+" & Level_Str (Fun_Call) & ")?"
137+
& "(+" & Level_Str (GExpr) & ")?";
137138
end Source_Level_Options;
138139

139140
-------------------------------------
@@ -149,6 +150,10 @@ package body Coverage_Options is
149150
-- Register the coverage level Combinaison combined with function and
150151
-- call coverage.
151152

153+
procedure Add_GExpr_Coverage_Level (Combinaison : Levels_Type);
154+
-- Register the coverage level Combinaison combined with guarded
155+
-- expression coverage.
156+
152157
---------------------------------
153158
-- Add_Fun_Call_Coverage_Level --
154159
---------------------------------
@@ -187,6 +192,21 @@ package body Coverage_Options is
187192
end loop;
188193
end Add_Assert_Coverage_Levels;
189194

195+
------------------------------
196+
-- Add_GExpr_Coverage_Level --
197+
------------------------------
198+
199+
procedure Add_GExpr_Coverage_Level (Combinaison : Levels_Type) is
200+
Comb : Levels_Type := Combinaison;
201+
begin
202+
-- Activate GExpr to combine it with the levels in Comb
203+
Comb (GExpr) := True;
204+
205+
Add_Source_Level_Option (Comb);
206+
Add_Fun_Call_Coverage_Level (Comb);
207+
Add_Assert_Coverage_Levels (Comb);
208+
end Add_GExpr_Coverage_Level;
209+
190210
Decision_Levels : constant array (1 .. 3) of Coverage_Level :=
191211
(Decision, MCDC, UC_MCDC);
192212

@@ -199,6 +219,7 @@ package body Coverage_Options is
199219
Add_Source_Level_Option (Combinaison);
200220
Add_Fun_Call_Coverage_Level (Combinaison);
201221
Add_Assert_Coverage_Levels (Combinaison);
222+
Add_GExpr_Coverage_Level (Combinaison);
202223

203224
-- Do the same for all other regular source coverage options
204225

@@ -210,6 +231,7 @@ package body Coverage_Options is
210231
Add_Source_Level_Option (Combinaison);
211232
Add_Fun_Call_Coverage_Level (Combinaison);
212233
Add_Assert_Coverage_Levels (Combinaison);
234+
Add_GExpr_Coverage_Level (Combinaison);
213235

214236
-- Deactivate Lvl to combine the next level with "stmt"
215237
Combinaison (Lvl) := False;

Diff for: ‎tools/gnatcov/coverage_options.ads

+20-11
Original file line numberDiff line numberDiff line change
@@ -28,19 +28,21 @@ package Coverage_Options is
2828
use all type Unbounded_String;
2929

3030
type Coverage_Level is
31-
(Insn, Branch, Stmt, Decision, MCDC, UC_MCDC, ATC, ATCC, Fun_Call);
31+
(Insn, Branch, Stmt, Decision, MCDC, UC_MCDC, ATC, ATCC, Fun_Call,
32+
GExpr);
3233
-- Coverage objectives supported by xcov. The following values are
3334
-- supported:
3435

35-
-- * object coverage at instruction level (Insn);
36-
-- * object coverage at branch level (Branch);
37-
-- * source coverage at statement level (Stmt);
38-
-- * source coverage at decision level (Decision);
39-
-- * source coverage at masking MC/DC level (MCDC);
40-
-- * source coverage at unique cause MC/DC level (UC_MCDC);
41-
-- * source coverage at ATC level (ATC);
42-
-- * source coverage at ATCC level (ATCC).
43-
-- * source coverage at Call level (Fun_Call)
36+
-- * object coverage at instruction level (Insn);
37+
-- * object coverage at branch level (Branch);
38+
-- * source coverage at statement level (Stmt);
39+
-- * source coverage at decision level (Decision);
40+
-- * source coverage at masking MC/DC level (MCDC);
41+
-- * source coverage at unique cause MC/DC level (UC_MCDC);
42+
-- * source coverage at ATC level (ATC);
43+
-- * source coverage at ATCC level (ATCC);
44+
-- * source coverage at Call level (Fun_Call);
45+
-- * source coverage at Guarded Expressions level (GExpr).
4446

4547
-- The terms "instruction", "branch", "statement", "decision" and "MCDC"
4648
-- should be understood here as they are defined in the DO-178B standard;
@@ -63,9 +65,16 @@ package Coverage_Options is
6365
--
6466
-- * Call coverage : a call is covered if it was executed as least
6567
-- once.
68+
--
69+
-- The "GExpr" coverage criteria (short for Guarded Expressions) serves the
70+
-- purpose of tracking the exhaustive execution of all branches of
71+
-- conditional expressions (case-expr and if-expr) and to ensure the
72+
-- execution the dependent expression of quantified expressions
73+
-- (for some and for all), which may not run if executed against an empty
74+
-- array.
6675

6776
subtype Object_Coverage_Level is Coverage_Level range Insn .. Branch;
68-
subtype Source_Coverage_Level is Coverage_Level range Stmt .. Fun_Call;
77+
subtype Source_Coverage_Level is Coverage_Level range Stmt .. GExpr;
6978
subtype MCDC_Coverage_Level is Coverage_Level range MCDC .. UC_MCDC;
7079
subtype Contract_Condition_Level is Coverage_Level range ATCC .. ATCC;
7180

Diff for: ‎tools/gnatcov/files_table.ads

+7-6
Original file line numberDiff line numberDiff line change
@@ -224,7 +224,7 @@ package Files_Table is
224224
-- Exec from where the address range has been extracted
225225
end record;
226226

227-
type Line_State_Cell is (Cell_1, Cell_2, Cell_3, Cell_4);
227+
type Line_State_Cell is (Cell_1, Cell_2, Cell_3, Cell_4, Cell_5);
228228

229229
Coverage_Level_To_Cell : constant
230230
array (Coverage_Level) of Line_State_Cell :=
@@ -236,13 +236,14 @@ package Files_Table is
236236
UC_MCDC => Cell_2,
237237
ATC => Cell_3,
238238
ATCC => Cell_3,
239-
Fun_Call => Cell_4);
239+
Fun_Call => Cell_4,
240+
GExpr => Cell_5);
240241
-- For one specific execution of GNATcov, we know that
241242
-- each line needs at most only four states (insn, branch,
242-
-- stmt(+decision|+mcdc|+uc_mcdc)?(+atc|+atcc)?(funcall)?). Thus, there is
243-
-- no need to store the state for all coverage levels at the same time.
244-
-- This table is thus used to convert the coverage level to the appropriate
245-
-- state "storage cell".
243+
-- stmt(+decision|+mcdc|+uc_mcdc)?(+atc|+atcc)?(funcall)?(+gexpr)?).
244+
-- Thus, there is no need to store the state for all coverage levels at the
245+
-- same time. This table is thus used to convert the coverage level to the
246+
-- appropriate state "storage cell".
246247

247248
type Line_States is array (Line_State_Cell) of Line_State;
248249

0 commit comments

Comments
 (0)
Please sign in to comment.