From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 129381 invoked by alias); 9 Nov 2017 12:11:19 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Received: (qmail 129368 invoked by uid 89); 9 Nov 2017 12:11:19 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-9.4 required=5.0 tests=AWL,BAYES_00,GIT_PATCH_2,GIT_PATCH_3,KAM_ASCII_DIVIDERS,RCVD_IN_DNSWL_NONE,SPF_PASS,UNSUBSCRIBE_BODY autolearn=ham version=3.3.2 spammy=justify, Hex X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Thu, 09 Nov 2017 12:11:16 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 6291656A04; Thu, 9 Nov 2017 07:11:15 -0500 (EST) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id NZ9W0OfTYkBY; Thu, 9 Nov 2017 07:11:15 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 52420567DC; Thu, 9 Nov 2017 07:11:15 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4862) id 514113F0; Thu, 9 Nov 2017 07:11:15 -0500 (EST) Date: Thu, 09 Nov 2017 12:21:00 -0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Rewrite code and add justifications for static analysis Message-ID: <20171109121115.GA31534@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="qMm9M+Fa2AknHoGS" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes X-SW-Source: 2017-11/txt/msg00738.txt.bz2 --qMm9M+Fa2AknHoGS Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-length: 910 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 * 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. --qMm9M+Fa2AknHoGS Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename=difs Content-length: 3122 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; --qMm9M+Fa2AknHoGS--