diff mbox series

[Ada] Rewrite code and add justifications for static analysis

Message ID 20171109121115.GA31534@adacore.com
State New
Headers show
Series [Ada] Rewrite code and add justifications for static analysis | expand

Commit Message

Pierre-Marie de Rodat Nov. 9, 2017, 12:11 p.m. UTC 
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  <moy@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.
diff mbox series

Patch

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;