From patchwork Mon Apr 18 12:34:00 2016 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 611729 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 3qpSJF57jDz9t74 for ; Mon, 18 Apr 2016 22:34:20 +1000 (AEST) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=w4UBqUOv; dkim-atps=neutral DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=jvBLklVOhqqfmiMqBQY6QLbk5wk3st2a/6IAuYyJT2D7GR0pJ9 t6JytSB3ePgA2NPh8+eXxZoLYZlVCc7ILSRvPb8kx3j+OWBp9CbNfFlhst+txCl4 iUXWHmIJ7v9D8sx/YA4d6uIguMalP/FnFd6nY8TpRvexSwj02rBnSg5k8= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=EGl3X1yOQQ4hhnsYVmAEKT0DoWw=; b=w4UBqUOvosCqGg4A5Y8P i5ZRzY1dyHSlrmn0DnKjIq38dwYColCqF0ar7xLaNfjCIKjsbAaffZVqKfs4H+mH TXi3i7M9cgJ0Y3F+E3zFlbcrTIsaCzhroIrx8EeugdsH131RLlUnLxItaTOHzq3H SS6DX8e5xQhtJscOL0/yqyQ= Received: (qmail 113655 invoked by alias); 18 Apr 2016 12:34:13 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 113626 invoked by uid 89); 18 Apr 2016 12:34:12 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=2.4 required=5.0 tests=AWL, BAYES_50, KAM_ASCII_DIVIDERS, KAM_LAZY_DOMAIN_SECURITY, RCVD_IN_DNSWL_NONE autolearn=no version=3.3.2 spammy=D*adacore.com, Entity_Id, entity_id, Present 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 (AES256-SHA encrypted) ESMTPS; Mon, 18 Apr 2016 12:34:02 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id C9E9A116901; Mon, 18 Apr 2016 08:34:00 -0400 (EDT) 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 U1U5AiIUVchA; Mon, 18 Apr 2016 08:34:00 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id B48021168FB; Mon, 18 Apr 2016 08:34:00 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id AF1CB181; Mon, 18 Apr 2016 08:34:00 -0400 (EDT) Date: Mon, 18 Apr 2016 08:34:00 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Issue check instead of error in static division by zero Message-ID: <20160418123400.GA51550@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) In some cases of generic instantiations, or code configuration, some code may be deactivated and contain static divisions by zero. Instead of issuing an error in SPARK code, generate a suitable check. Tested on x86_64-pc-linux-gnu, committed on trunk 2016-04-18 Yannick Moy * sem_eval.adb (Eval_Arithmetic_Op): Do not issue error on static division by zero, instead possibly issue a warning. * sem_res.adb (Resolve_Arithmetic_Op): Do not issue error on static division by zero, instead add check flag on original expression. * sem_util.adb, sem_util.ads (Compile_Time_Constraint_Error): Only issue error when both SPARK_Mode is On and Warn is False. Index: sem_util.adb =================================================================== --- sem_util.adb (revision 235122) +++ sem_util.adb (working copy) @@ -4574,9 +4574,16 @@ begin -- If this is a warning, convert it into an error if we are in code - -- subject to SPARK_Mode being set ON. + -- subject to SPARK_Mode being set On, unless Warn is True to force a + -- warning. The rationale is that a compile-time constraint error should + -- lead to an error instead of a warning when SPARK_Mode is On, but in + -- a few cases we prefer to issue a warning and generate both a suitable + -- run-time error in GNAT and a suitable check message in GNATprove. + -- Those cases are those that likely correspond to deactivated SPARK + -- code, so that this kind of code can be compiled and analyzed instead + -- of being rejected. - Error_Msg_Warn := SPARK_Mode /= On; + Error_Msg_Warn := Warn or SPARK_Mode /= On; -- A static constraint error in an instance body is not a fatal error. -- we choose to inhibit the message altogether, because there is no @@ -4648,8 +4655,6 @@ -- evaluated. if not Is_Statically_Unevaluated (N) then - Error_Msg_Warn := SPARK_Mode /= On; - if Present (Ent) then Error_Msg_NEL (Msgc (1 .. Msgl), N, Ent, Eloc); else Index: sem_util.ads =================================================================== --- sem_util.ads (revision 235122) +++ sem_util.ads (working copy) @@ -135,7 +135,9 @@ -- is present, this is used instead. Warn is normally False. If it is -- True then the message is treated as a warning even though it does -- not end with a ? (this is used when the caller wants to parameterize - -- whether an error or warning is given). + -- whether an error or warning is given), or when the message should be + -- treated as a warning even when SPARK_Mode is On (which otherwise would + -- force an error). function Async_Readers_Enabled (Id : Entity_Id) return Boolean; -- Given the entity of an abstract state or a variable, determine whether Index: sem_res.adb =================================================================== --- sem_res.adb (revision 235116) +++ sem_res.adb (working copy) @@ -5440,7 +5440,9 @@ and then Expr_Value_R (Rop) = Ureal_0)) then -- Specialize the warning message according to the operation. - -- The following warnings are for the case + -- When SPARK_Mode is On, force a warning instead of an error + -- in that case, as this likely corresponds to deactivated + -- code. The following warnings are for the case case Nkind (N) is when N_Op_Divide => @@ -5459,23 +5461,26 @@ ("float division by zero, may generate " & "'+'/'- infinity??", Right_Opnd (N)); - -- For all other cases, we get a Constraint_Error + -- For all other cases, we get a Constraint_Error else Apply_Compile_Time_Constraint_Error (N, "division by zero??", CE_Divide_By_Zero, - Loc => Sloc (Right_Opnd (N))); + Loc => Sloc (Right_Opnd (N)), + Warn => SPARK_Mode = On); end if; when N_Op_Rem => Apply_Compile_Time_Constraint_Error (N, "rem with zero divisor??", CE_Divide_By_Zero, - Loc => Sloc (Right_Opnd (N))); + Loc => Sloc (Right_Opnd (N)), + Warn => SPARK_Mode = On); when N_Op_Mod => Apply_Compile_Time_Constraint_Error (N, "mod with zero divisor??", CE_Divide_By_Zero, - Loc => Sloc (Right_Opnd (N))); + Loc => Sloc (Right_Opnd (N)), + Warn => SPARK_Mode = On); -- Division by zero can only happen with division, rem, -- and mod operations. @@ -5484,6 +5489,13 @@ raise Program_Error; end case; + -- In GNATprove mode, we enable the division check so that + -- GNATprove will issue a message if it cannot be proved. + + if GNATprove_Mode then + Activate_Division_Check (N); + end if; + -- Otherwise just set the flag to check at run time else Index: sem_eval.adb =================================================================== --- sem_eval.adb (revision 235124) +++ sem_eval.adb (working copy) @@ -1885,9 +1885,14 @@ -- division, rem and mod if the right operand is zero. if Right_Int = 0 then + + -- When SPARK_Mode is On, force a warning instead of + -- an error in that case, as this likely corresponds + -- to deactivated code. + Apply_Compile_Time_Constraint_Error (N, "division by zero", CE_Divide_By_Zero, - Warn => not Stat); + Warn => not Stat or SPARK_Mode = On); Set_Raises_Constraint_Error (N); return; @@ -1903,10 +1908,16 @@ -- division, rem and mod if the right operand is zero. if Right_Int = 0 then + + -- When SPARK_Mode is On, force a warning instead of + -- an error in that case, as this likely corresponds + -- to deactivated code. + Apply_Compile_Time_Constraint_Error (N, "mod with zero divisor", CE_Divide_By_Zero, - Warn => not Stat); + Warn => not Stat or SPARK_Mode = On); return; + else Result := Left_Int mod Right_Int; end if; @@ -1917,9 +1928,14 @@ -- division, rem and mod if the right operand is zero. if Right_Int = 0 then + + -- When SPARK_Mode is On, force a warning instead of + -- an error in that case, as this likely corresponds + -- to deactivated code. + Apply_Compile_Time_Constraint_Error (N, "rem with zero divisor", CE_Divide_By_Zero, - Warn => not Stat); + Warn => not Stat or SPARK_Mode = On); return; else