From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: (qmail 68999 invoked by alias); 12 Nov 2015 11:38:55 -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 68923 invoked by uid 89); 12 Nov 2015 11:38:55 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=0.3 required=5.0 tests=AWL,BAYES_50,KAM_ASCII_DIVIDERS,KAM_LAZY_DOMAIN_SECURITY,RCVD_IN_DNSWL_LOW autolearn=no version=3.3.2 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; Thu, 12 Nov 2015 11:38:51 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 5465229954; Thu, 12 Nov 2015 06:38:49 -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 QR-aBFRRwQLN; Thu, 12 Nov 2015 06:38:49 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 4478C29953; Thu, 12 Nov 2015 06:38:49 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4192) id 4359B1A5; Thu, 12 Nov 2015 06:38:49 -0500 (EST) Date: Thu, 12 Nov 2015 11:38:00 -0000 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Obscure messages due to freezing of contracts Message-ID: <20151112113849.GA44751@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="oyUTqETQ0mS9luUI" Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-SW-Source: 2015-11/txt/msg01494.txt.bz2 --oyUTqETQ0mS9luUI Content-Type: text/plain; charset=us-ascii Content-Disposition: inline Content-length: 2946 This patch classifies a misplaced constituent as a critical error and stops the compilation. This ensures that the missing link between a constituent and state will not cause obscure cascaded errors. ------------ -- Source -- ------------ -- pack.ads package Pack with Spark_Mode => On, Abstract_State => Top_State, Initializes => Top_State is procedure Do_Something (Value : in out Natural; Success : out Boolean) with Global => (In_Out => Top_State), Depends => (Value =>+ Top_State, Success => (Value, Top_State), Top_State =>+ Value); end Pack; -- pack.adb package body Pack with SPARK_Mode => On, Refined_State => (Top_State => (Count, A_Pack.State)) is package A_Pack with Abstract_State => State, Initializes => State is procedure A_Proc (Test : in out Natural) with Global => (In_Out => State), Depends => (Test =>+ State, State =>+ Test); end A_Pack; package body A_Pack with Refined_State => (State => Total) is Total : Natural := 0; procedure A_Proc (Test : in out Natural) with Refined_Global => (In_Out => Total), Refined_Depends => ((Test =>+ Total, Total =>+ Test)) is begin if Total > Natural'Last - Test then Total := abs (Total - Test); else Total := Total + Test; end if; Test := Total; end A_Proc; end A_Pack; Count : Natural := 0; procedure Do_Something (Value : in out Natural; Success : out Boolean) with Refined_Global => (In_Out => (Count, A_Pack.State)), Refined_Depends => (Value =>+ (Count, A_Pack.State), Success => (Value, Count, A_Pack.State), Count =>+ null, A_Pack.State =>+ (Count, Value)) is begin Count := Count rem 128; if Count <= Value then Value := Count + (Value - Count) / 2; else Value := Value + (Count - Value) / 2; end if; A_Pack.A_Proc (Value); Success := Value /= 0; end Do_Something; end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c pack.adb pack.adb:3:09: body "A_Pack" declared at line 15 freezes the contract of "Pack" pack.adb:3:09: all constituents must be declared before body at line 15 pack.adb:3:41: "Count" is undefined compilation abandoned due to previous error Tested on x86_64-pc-linux-gnu, committed on trunk 2015-11-12 Hristian Kirtchev * sem_prag.adb (Analyze_Constituent): Stop the analysis after detecting a misplaced constituent as this is a critical error. --oyUTqETQ0mS9luUI Content-Type: text/plain; charset=us-ascii Content-Disposition: attachment; filename=difs Content-length: 859 Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 230236) +++ sem_prag.adb (working copy) @@ -25408,6 +25408,14 @@ SPARK_Msg_N ("\all constituents must be declared before body #", N); + + -- A misplaced constituent is a critical error because + -- pragma Refined_Depends or Refined_Global depends on + -- the proper link between a state and a constituent. + -- Stop the compilation, as this leads to a multitude + -- of misleading cascaded errors. + + raise Program_Error; end if; -- The constituent is a valid state or object --oyUTqETQ0mS9luUI--