[Ada] Rewrite code and add justifications for static analysis

[Ada] Rewrite code and add justifications for static analysis

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 910 bytes --]

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.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 3122 bytes --]

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;