CodePeer static analyzer issues messages that can be avoided by
simpliflying the code, or justifying the false positives.
There is no test, as this does no impact the behavior of the compiler.
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-11-09 Yannick Moy <m...@adacore.com>
* erroutc.adb (Output_Error_Msgs): Justify CodePeer false positive
message.
* gnatbind.adb (Scan_Bind_Arg): Simplify test to remove always true
condition.
* namet.adb (Copy_One_Character): Add assumption for static analysis,
as knowledge that Hex(2) is in the range 0..255 is too complex for
CodePeer.
(Finalize): Add assumption for static analysis, as the fact that there
are symbols in the table depends on a global invariant at this point in
the program.
* set_targ.adb (Check_Spaces): Justify CodePeer false positive message.
* stylesw.adb (Save_Style_Check_Options): Rewrite to avoid test always
true.
Index: set_targ.adb
===================================================================
--- set_targ.adb (revision 254570)
+++ set_targ.adb (working copy)
@@ -604,6 +604,10 @@
procedure Check_Spaces is
begin
if N > Buflen or else Buffer (N) /= ' ' then
+ pragma Annotate
+ (CodePeer, False_Positive, "condition predetermined",
+ "N may be less than Buflen when calling Check_Spaces");
+
FailN ("missing space for");
end if;
Index: erroutc.adb
===================================================================
--- erroutc.adb (revision 254563)
+++ erroutc.adb (working copy)
@@ -512,6 +512,9 @@
-- so now we output a tab to match up with the text.
if Src (P) = ASCII.HT then
+ pragma Annotate
+ (CodePeer, False_Positive, "validity check",
+ "Src(P) is initialized at this point");
Write_Char (ASCII.HT);
P := P + 1;
Index: gnatbind.adb
===================================================================
--- gnatbind.adb (revision 254563)
+++ gnatbind.adb (working copy)
@@ -330,9 +330,7 @@
then
Output_File_Name_Seen := True;
- if Argv'Length = 0
- or else (Argv'Length >= 1 and then Argv (1) = '-')
- then
+ if Argv'Length = 0 or else Argv (1) = '-' then
Fail ("output File_Name missing after -o");
else
Index: namet.adb
===================================================================
--- namet.adb (revision 254571)
+++ namet.adb (working copy)
@@ -258,7 +258,13 @@
-- simply use their normal representation.
else
- Insert_Character (Character'Val (Hex (2)));
+ declare
+ W2 : constant Word := Hex (2);
+ begin
+ pragma Assume (W2 <= 255);
+ -- Add assumption to facilitate static analysis
+ Insert_Character (Character'Val (W2));
+ end;
end if;
-- WW (wide wide character insertion)
@@ -753,6 +759,9 @@
Write_Eol;
Write_Str ("Average number of probes for lookup = ");
+ pragma Assume (Nsyms /= 0);
+ -- Add assumption to facilitate static analysis. Here Nsyms cannot be
+ -- zero because many symbols are added to the table by default.
Probes := Probes / Nsyms;
Write_Int (Probes / 200);
Write_Char ('.');
Index: stylesw.adb
===================================================================
--- stylesw.adb (revision 254570)
+++ stylesw.adb (working copy)
@@ -161,7 +161,8 @@
if Style_Check_Comments then
if Style_Check_Comments_Spacing = 2 then
Add ('c', Style_Check_Comments);
- elsif Style_Check_Comments_Spacing = 1 then
+ else
+ pragma Assert (Style_Check_Comments_Spacing = 1);
Add ('C', Style_Check_Comments);
end if;
end if;
