From patchwork Thu Apr 27 10:55:25 2017 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 755965 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 3wDDPl5pHlz9sNP for ; Thu, 27 Apr 2017 20:55:38 +1000 (AEST) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="pMqSB/7o"; 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=jS7gLZLUPBNz9H9OERwH1VyTlV178cyXXAFV5A+wwTz0f3p2gK wfdXvuHmYBl+mE2xvj/Q3cC5v9kn01eEzu6zKb/G1N+SYybw3PQbsS43szSm12F4 dyS5how5/2I0FYae/xKIx+WTFe1AmQOE3YfffBPC9oah0Mt9ocAbC5JRQ= 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=3Km2dijCET7SDa7ceBSkzenDD8E=; b=pMqSB/7o3gnuCYFR3goR q1n7R9tH24ffz4T0s90jeTPR0VAyqhS1Udpadvsxdt1dDWR57IECmnOYW98Eaonn wJQI/oreQnayHPUQ9qOiv1RDsyDvsz4u7yLSU0Fg8AyVz5Ehf7TGgrUw6RaRtQ2i GIQv3WQB0YpJ5ZEmviOJ2Ow= Received: (qmail 79109 invoked by alias); 27 Apr 2017 10:55:27 -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 79090 invoked by uid 89); 27 Apr 2017 10:55:26 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.0 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy= 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, 27 Apr 2017 10:55:24 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 22E763E53; Thu, 27 Apr 2017 06:55:25 -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 lqi80LQbuJ6T; Thu, 27 Apr 2017 06:55:25 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 138C95A5C6; Thu, 27 Apr 2017 06:55:25 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4192) id 0E6533F0; Thu, 27 Apr 2017 06:55:25 -0400 (EDT) Date: Thu, 27 Apr 2017 06:55:25 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Fix evaluation of comparisons for GNATprove Message-ID: <20170427105525.GA3946@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) Static analysis tools benefit from some evaluations being done in frontend, in particular comparisons between values of universal types which are supposed to be evaluated at compile time and which static analysis tools like GNATprove may not support. Restore such evaluation during semantic analysis for arguments of universal types, which was disabled previously inside assertions to provide static analysis tools with more information (but still disable when arguments are not of universal type). Tested on x86_64-pc-linux-gnu, committed on trunk 2017-04-27 Yannick Moy * sem_res.adb (Resolve_Comparison_Op): Always evaluate comparisons between values of universal types. Index: sem_res.adb =================================================================== --- sem_res.adb (revision 247312) +++ sem_res.adb (working copy) @@ -6927,8 +6927,15 @@ -- this Eval call may change N to True/False. Skip this evaluation -- inside assertions, in order to keep assertions as written by users -- for tools that rely on these, e.g. GNATprove for loop invariants. + -- Except evaluation is still performed even inside assertions for + -- comparisons between values of universal type, which are useless + -- for static analysis tools, and not supported even by GNATprove. - if In_Assertion_Expr = 0 then + if In_Assertion_Expr = 0 + or else (Is_Universal_Numeric_Type (Etype (L)) + and then + Is_Universal_Numeric_Type (Etype (R))) + then Eval_Relational_Op (N); end if; end Resolve_Comparison_Op;