From patchwork Mon Mar 2 09:24:48 2015 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 444985 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 F1593140172 for ; Mon, 2 Mar 2015 20:25:43 +1100 (AEDT) Authentication-Results: ozlabs.org; dkim=pass reason="1024-bit key; unprotected key" header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b=IoPhMNir; dkim-adsp=none (unprotected policy); 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=IFwJssGwc9+MB8Xroer6yeJivz0/vjVwNC9VhbJQ5+KazYHhxP 940xLyA3RS2UKqtBJU609Ie4HGVwySf4f/pQ5BZTw0rFTo6EUD9G/S5g/ZOzDN8i Md4PgFVpY5YTOE9Lab/RysDBLZ/A8yLvhy0XO8Wdw4EBnBeOhr8YHjA+M= 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=3VPFsozd8KROYXIKfWrs2vanjsA=; b=IoPhMNirS9g9bfyJlguh zk2isROSTef2SQi1CU06y9vNzdRcV9oTy57ituYNtWUerg4fjXCg7cE+O0DvDmU+ NAsAWX3NHr29OILJkjb+8KjaOLtApTe996dcuasQj7HmgtLGYWbrhEk6u0hqynj/ 4GvxZavACBB+zicuAxJ54AM= Received: (qmail 107923 invoked by alias); 2 Mar 2015 09:25:19 -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 107783 invoked by uid 89); 2 Mar 2015 09:25:17 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=2.6 required=5.0 tests=AWL, BAYES_50, FILL_THIS_FORM, FILL_THIS_FORM_LOAN, FILL_THIS_FORM_LONG, FORM_FRAUD 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; Mon, 02 Mar 2015 09:24:51 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id C3A8BD3225; Mon, 2 Mar 2015 04:24:48 -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 MVdFB2+kFxXj; Mon, 2 Mar 2015 04:24:48 -0500 (EST) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 8A3B2D2FFC; Mon, 2 Mar 2015 04:24:48 -0500 (EST) Received: by kwai.gnat.com (Postfix, from userid 4192) id 86FF93FE3B; Mon, 2 Mar 2015 04:24:48 -0500 (EST) Date: Mon, 2 Mar 2015 04:24:48 -0500 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Subprogram contracts on generics Message-ID: <20150302092448.GA22893@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) This is a multi purpose patch concerning the contracts on subprograms. * The patch implements "instantiatable contracts", in other words SPARK- related contract annotations can now appear on generic subprogram and be instantiated as part of the subprogram instantiation. * The patch removes multiple kludges for ASIS. * The patch removes multiple kludges concerning the analysis and global reference storage for contracts related to generic subprograms. * The patch fixes multiple issies with respect to contracts on subprograms and subprogram bodies that act as compilation units. * The patch cleans up a lot of dubious and fragmented code. ------------ -- Source -- ------------ -- body_and_spec.ads with Refs; function Body_And_Spec (Input : Integer) return Integer with Pre => Input + Refs.External_Zero > 1, Post => Body_And_Spec'Result + Refs.External_Zero > 5; -- body_and_spec.adb function Body_And_Spec (Input : Integer) return Integer is begin return Input + 1; end Body_And_Spec; -- body_and_spec_pragmas.ads with Refs; function Body_And_Spec_Pragmas (Input : Integer) return Integer; pragma Precondition (Input + Refs.External_Zero > 1); pragma Postcondition (Body_And_Spec_Pragmas'Result + Refs.External_Zero > 5); -- body_and_spec_pragmas.adb function Body_And_Spec_Pragmas (Input : Integer) return Integer is pragma Precondition (Input + Refs.External_Zero > 2); pragma Postcondition (Body_And_Spec_Pragmas'Result + Refs.External_Zero > 4); begin return Input + 1; end Body_And_Spec_Pragmas; -- body_only.adb with Refs; function Body_Only (Input : Integer) return Integer with Pre => Input + Refs.External_Zero > 2, Post => Body_Only'Result + Refs.External_Zero > 4 is begin return Input + 1; end Body_Only; -- body_only_pragmas.adb function Body_Only_Pragmas (Input : Integer) return Integer is pragma Pre (Input > 2); pragma Post (Body_Only_Pragmas'Result > 4); begin return Input + 1; end Body_Only_Pragmas; -- gen_body_and_spec.ads with Refs; generic Zero : Integer; function Gen_Body_And_Spec (Input : Integer) return Integer with Pre => Input + Zero + Refs.External_Zero > 1, Post => Gen_Body_And_Spec'Result + Zero + Refs.External_Zero > 5; -- gen_body_and_spec.adb function Gen_Body_And_Spec (Input : Integer) return Integer is begin return Input + 1; end Gen_Body_And_Spec; -- gen_body_and_spec_pragmas.ads with Refs; generic Zero : Integer; function Gen_Body_And_Spec_Pragmas (Input : Integer) return Integer; pragma Precondition (Input + Zero + Refs.External_Zero > 1); pragma Postcondition (Gen_Body_And_Spec_Pragmas'Result + Zero + Refs.External_Zero > 5); -- gen_body_and_spec_pragmas.adb function Gen_Body_And_Spec_Pragmas (Input : Integer) return Integer is pragma Precondition (Input + Zero + Refs.External_Zero > 2); pragma Postcondition (Gen_Body_And_Spec_Pragmas'Result + Zero + Refs.External_Zero > 4); begin return Input + 1; end Gen_Body_And_Spec_Pragmas; -- gen_pack.ads with Refs; generic Zero : Integer; package Gen_Pack is function Func (Input : Integer) return Integer with Pre => Input + Zero + Refs.External_Zero > 1, Post => Func'Result + Zero + Refs.External_Zero > 5; end Gen_Pack; -- gen_pack.adb package body Gen_Pack is function Func (Input : Integer) return Integer is begin return Input + 1; end Func; end Gen_Pack; -- gen_pack_gen.ads with Refs; generic Zero : Integer; package Gen_Pack_Gen is generic Local_Zero : Integer; function Func (Input : Integer) return Integer with Pre => Input + Zero + Local_Zero + Refs.External_Zero > 1, Post => Func'Result + Zero + Local_Zero + Refs.External_Zero > 5; end Gen_Pack_Gen; -- gen_pack_gen.adb package body Gen_Pack_Gen is function Func (Input : Integer) return Integer is begin return Input + 1; end Func; end Gen_Pack_Gen; -- gen_pack_gen_pragmas.ads with Refs; generic Zero : Integer; package Gen_Pack_Gen_Pragmas is generic Local_Zero : Integer; function Func (Input : Integer) return Integer; pragma Precondition (Input + Zero + Local_Zero + Refs.External_Zero > 1); pragma Postcondition (Func'Result + Zero + Local_Zero + Refs.External_Zero > 5); end Gen_Pack_Gen_Pragmas; -- gen_pack_gen_pragmas.adb package body Gen_Pack_Gen_Pragmas is function Func (Input : Integer) return Integer is pragma Precondition (Input + Zero + Local_Zero + Refs.External_Zero > 2); pragma Postcondition (Func'Result + Zero + Local_Zero + Refs.External_Zero > 4); begin return Input + 1; end Func; end Gen_Pack_Gen_Pragmas; -- gen_pack_pragmas.ads with Refs; generic Zero : Integer; package Gen_Pack_Pragmas is function Func (Input : Integer) return Integer; pragma Precondition (Input + Zero + Refs.External_Zero > 1); pragma Postcondition (Func'Result + Zero + Refs.External_Zero > 5); end Gen_Pack_Pragmas; -- gen_pack_pragmas.adb package body Gen_Pack_Pragmas is function Func (Input : Integer) return Integer is pragma Precondition (Input + Zero + Refs.External_Zero > 2); pragma Postcondition (Func'Result + Zero + Refs.External_Zero > 4); begin return Input + 1; end Func; end Gen_Pack_Pragmas; -- pack.ads with Refs; package Pack is function Func (Input : Integer) return Integer with Pre => Input + Refs.External_Zero > 1, Post => Func'Result + Refs.External_Zero > 5; end Pack; -- pack.adb package body Pack is function Func (Input : Integer) return Integer is begin return Input + 1; end Func; end Pack; -- pack_gen.ads with Refs; package Pack_Gen is generic Zero : Integer; function Func (Input : Integer) return Integer with Pre => Input + Zero + Refs.External_Zero > 1, Post => Func'Result + Zero + Refs.External_Zero > 5; end Pack_Gen; -- pack_gen.adb package body Pack_Gen is function Func (Input : Integer) return Integer is begin return Input + 1; end Func; end Pack_Gen; -- pack_gen_pragmas.ads with Refs; package Pack_Gen_Pragmas is generic Zero : Integer; function Func (Input : Integer) return Integer; pragma Precondition (Input + Zero + Refs.External_Zero > 1); pragma Postcondition (Func'Result + Zero + Refs.External_Zero > 5); end Pack_Gen_Pragmas; -- pack_gen_pragmas.adb package body Pack_Gen_Pragmas is function Func (Input : Integer) return Integer is pragma Precondition (Input + Zero + Refs.External_Zero > 2); pragma Postcondition (Func'Result + Zero + Refs.External_Zero > 4); begin return Input + 1; end Func; end Pack_Gen_Pragmas; -- pack_pragmas.ads with Refs; package Pack_Pragmas is function Func (Input : Integer) return Integer; pragma Precondition (Input + Refs.External_Zero > 1); pragma Postcondition (Func'Result + Refs.External_Zero > 5); end Pack_Pragmas; -- pack_pragmas.adb package body Pack_Pragmas is function Func (Input : Integer) return Integer is pragma Precondition (Input + Refs.External_Zero > 2); pragma Postcondition (Func'Result + Refs.External_Zero > 4); begin return Input + 1; end Func; end Pack_Pragmas; -- refs.ads package Refs is External_Zero : Integer := 0; end Refs; -- main.adb with Ada.Assertions; use Ada.Assertions; with Ada.Exceptions; use Ada.Exceptions; with Ada.Text_IO; use Ada.Text_IO; with Body_And_Spec; with Body_And_Spec_Pragmas; with Body_Only; with Body_Only_Pragmas; with Gen_Body_And_Spec; with Gen_Body_And_Spec_Pragmas; with Gen_Pack; with Gen_Pack_Pragmas; with Gen_Pack_Gen; with Gen_Pack_Gen_Pragmas; with Pack; with Pack_Pragmas; with Pack_Gen; with Pack_Gen_Pragmas; procedure Main is Fail_Spec_Pre : constant Integer := 1; Fail_Body_Pre : constant Integer := 2; Fail_Body_Post : constant Integer := 3; Fail_Spec_Post : constant Integer := 4; OK : constant Integer := 5; Result : Integer; begin -- Aspects, body + spec begin Result := Body_And_Spec (Fail_Spec_Pre); Put_Line ("ERROR 1: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 1 " & Exception_Message (AE)); when others => Put_Line ("ERROR 1: unexpected exception"); end; begin Result := Body_And_Spec (Fail_Spec_Post); Put_Line ("ERROR 2: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 2 " & Exception_Message (AE)); when others => Put_Line ("ERROR 2: unexpected exception"); end; begin Result := Body_And_Spec (OK); Put_Line ("OK 3"); exception when others => Put_Line ("ERROR 3: unexpected exception"); end; -- Pragmas, body + spec begin Result := Body_And_Spec_Pragmas (Fail_Spec_Pre); Put_Line ("ERROR 4: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 4 " & Exception_Message (AE)); when others => Put_Line ("ERROR 4: unexpected exception"); end; begin Result := Body_And_Spec_Pragmas (Fail_Body_Pre); Put_Line ("ERROR 5: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 5 " & Exception_Message (AE)); when others => Put_Line ("ERROR 5: unexpected exception"); end; begin Result := Body_And_Spec_Pragmas (Fail_Body_Post); Put_Line ("ERROR 6: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 6 " & Exception_Message (AE)); when others => Put_Line ("ERROR 6: unexpected exception"); end; begin Result := Body_And_Spec_Pragmas (Fail_Spec_Post); Put_Line ("ERROR 7: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 7 " & Exception_Message (AE)); when others => Put_Line ("ERROR 7: unexpected exception"); end; begin Result := Body_And_Spec_Pragmas (OK); Put_Line ("OK 8"); exception when others => Put_Line ("ERROR 8: unexpected exception"); end; -- Aspects, body begin Result := Body_Only (Fail_Body_Pre); Put_Line ("ERROR 9: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 9 " & Exception_Message (AE)); when others => Put_Line ("ERROR 9: unexpected exception"); end; begin Result := Body_Only (Fail_Body_Post); Put_Line ("ERROR 10: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 10 " & Exception_Message (AE)); when others => Put_Line ("ERROR 10: unexpected exception"); end; begin Result := Body_Only (OK); Put_Line ("OK 11"); exception when others => Put_Line ("ERROR 11: unexpected exception"); end; -- Pragmas, body begin Result := Body_Only_Pragmas (Fail_Body_Pre); Put_Line ("ERROR 12: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 12 " & Exception_Message (AE)); when others => Put_Line ("ERROR 12: unexpected exception"); end; begin Result := Body_Only_Pragmas (Fail_Body_Post); Put_Line ("ERROR 13: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 13 " & Exception_Message (AE)); when others => Put_Line ("ERROR 13: unexpected exception"); end; begin Result := Body_Only_Pragmas (OK); Put_Line ("OK 14"); exception when others => Put_Line ("ERROR 14: unexpected exception"); end; -- Aspects, generic function declare function Func_Inst is new Gen_Body_And_Spec (0); begin begin Result := Func_Inst (Fail_Spec_Pre); Put_Line ("ERROR 15: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 15 " & Exception_Message (AE)); when others => Put_Line ("ERROR 15: unexpected exception"); end; begin Result := Func_Inst (Fail_Spec_Post); Put_Line ("ERROR 16: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 16 " & Exception_Message (AE)); when others => Put_Line ("ERROR 16: unexpected exception"); end; begin Result := Func_Inst (OK); Put_Line ("OK 17"); exception when others => Put_Line ("ERROR 17: unexpected exception"); end; end; -- Pragmas, generic function declare function Func_Inst is new Gen_Body_And_Spec_Pragmas (0); begin begin Result := Func_Inst (Fail_Spec_Pre); Put_Line ("ERROR 18: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 18 " & Exception_Message (AE)); when others => Put_Line ("ERROR 18: unexpected exception"); end; begin Result := Func_Inst (Fail_Body_Pre); Put_Line ("ERROR 19: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 19 " & Exception_Message (AE)); when others => Put_Line ("ERROR 19: unexpected exception"); end; begin Result := Func_Inst (Fail_Body_Post); Put_Line ("ERROR 20: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 20 " & Exception_Message (AE)); when others => Put_Line ("ERROR 20: unexpected exception"); end; begin Result := Func_Inst (Fail_Spec_Post); Put_Line ("ERROR 21: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 21 " & Exception_Message (AE)); when others => Put_Line ("ERROR 21: unexpected exception"); end; begin Result := Func_Inst (OK); Put_Line ("OK 22"); exception when others => Put_Line ("ERROR 22: unexpected exception"); end; end; -- Aspects, function in generic package declare package Pack_Inst is new Gen_Pack (0); begin begin Result := Pack_Inst.Func (Fail_Spec_Pre); Put_Line ("ERROR 23: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 23 " & Exception_Message (AE)); when others => Put_Line ("ERROR 23: unexpected exception"); end; begin Result := Pack_Inst.Func (Fail_Spec_Post); Put_Line ("ERROR 24: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 24 " & Exception_Message (AE)); when others => Put_Line ("ERROR 24: unexpected exception"); end; begin Result := Pack_Inst.Func (OK); Put_Line ("OK 25"); exception when others => Put_Line ("ERROR 25: unexpected exception"); end; end; -- Pragmas, function in generic package declare package Pack_Inst is new Gen_Pack_Pragmas (0); begin begin Result := Pack_Inst.Func (Fail_Spec_Pre); Put_Line ("ERROR 26: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 26 " & Exception_Message (AE)); when others => Put_Line ("ERROR 26: unexpected exception"); end; begin Result := Pack_Inst.Func (Fail_Body_Pre); Put_Line ("ERROR 27: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 27 " & Exception_Message (AE)); when others => Put_Line ("ERROR 27: unexpected exception"); end; begin Result := Pack_Inst.Func (Fail_Body_Post); Put_Line ("ERROR 28: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 28 " & Exception_Message (AE)); when others => Put_Line ("ERROR 28: unexpected exception"); end; begin Result := Pack_Inst.Func (Fail_Spec_Post); Put_Line ("ERROR 29: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 29 " & Exception_Message (AE)); when others => Put_Line ("ERROR 29: unexpected exception"); end; begin Result := Pack_Inst.Func (OK); Put_Line ("OK 30"); exception when others => Put_Line ("ERROR 30: unexpected exception"); end; end; -- Aspects, generic function in generic package declare package Pack_Inst is new Gen_Pack_Gen (0); function Func_Inst is new Pack_Inst.Func (0); begin begin Result := Func_Inst (Fail_Spec_Pre); Put_Line ("ERROR 31: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 31 " & Exception_Message (AE)); when others => Put_Line ("ERROR 31: unexpected exception"); end; begin Result := Func_Inst (Fail_Spec_Post); Put_Line ("ERROR 32: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 32 " & Exception_Message (AE)); when others => Put_Line ("ERROR 32: unexpected exception"); end; begin Result := Func_Inst (OK); Put_Line ("OK 33"); exception when others => Put_Line ("ERROR 33: unexpected exception"); end; end; -- Pragmas, generic function in generic package declare package Pack_Inst is new Gen_Pack_Gen_Pragmas (0); function Func_Inst is new Pack_Inst.Func (0); begin begin Result := Func_Inst (Fail_Spec_Pre); Put_Line ("ERROR 34: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 34 " & Exception_Message (AE)); when others => Put_Line ("ERROR 34: unexpected exception"); end; begin Result := Func_Inst (Fail_Body_Pre); Put_Line ("ERROR 35: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 35 " & Exception_Message (AE)); when others => Put_Line ("ERROR 35: unexpected exception"); end; begin Result := Func_Inst (Fail_Body_Post); Put_Line ("ERROR 36: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 36 " & Exception_Message (AE)); when others => Put_Line ("ERROR 36: unexpected exception"); end; begin Result := Func_Inst (Fail_Spec_Post); Put_Line ("ERROR 37: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 37 " & Exception_Message (AE)); when others => Put_Line ("ERROR 37: unexpected exception"); end; begin Result := Func_Inst (OK); Put_Line ("OK 38"); exception when others => Put_Line ("ERROR 35: unexpected exception"); end; end; -- Aspects, function in package begin Result := Pack.Func (Fail_Spec_Pre); Put_Line ("ERROR 39: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 39 " & Exception_Message (AE)); when others => Put_Line ("ERROR 39: unexpected exception"); end; begin Result := Pack.Func (Fail_Spec_Post); Put_Line ("ERROR 40: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 40 " & Exception_Message (AE)); when others => Put_Line ("ERROR 40: unexpected exception"); end; begin Result := Pack.Func (OK); Put_Line ("OK 41"); exception when others => Put_Line ("ERROR 41: unexpected exception"); end; -- Pragmas, function in package begin Result := Pack_Pragmas.Func (Fail_Spec_Pre); Put_Line ("ERROR 42: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 42 " & Exception_Message (AE)); when others => Put_Line ("ERROR 42: unexpected exception"); end; begin Result := Pack_Pragmas.Func (Fail_Body_Pre); Put_Line ("ERROR 43: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 43 " & Exception_Message (AE)); when others => Put_Line ("ERROR 43: unexpected exception"); end; begin Result := Pack_Pragmas.Func (Fail_Body_Post); Put_Line ("ERROR 44: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 44 " & Exception_Message (AE)); when others => Put_Line ("ERROR 44: unexpected exception"); end; begin Result := Pack_Pragmas.Func (Fail_Spec_Post); Put_Line ("ERROR 45: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 45 " & Exception_Message (AE)); when others => Put_Line ("ERROR 45: unexpected exception"); end; begin Result := Pack_Pragmas.Func (OK); Put_Line ("OK 46"); exception when others => Put_Line ("ERROR 46: unexpected exception"); end; -- Aspects, generic function in package declare function Func_Inst is new Pack_Gen.Func (0); begin begin Result := Func_Inst (Fail_Spec_Pre); Put_Line ("ERROR 47: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 47 " & Exception_Message (AE)); when others => Put_Line ("ERROR 47: unexpected exception"); end; begin Result := Func_Inst (Fail_Spec_Post); Put_Line ("ERROR 48: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 48 " & Exception_Message (AE)); when others => Put_Line ("ERROR 48: unexpected exception"); end; begin Result := Func_Inst (OK); Put_Line ("OK 49"); exception when others => Put_Line ("ERROR 41: unexpected exception"); end; end; -- Pragmas, generic function in package declare function Func_Inst is new Pack_Gen_Pragmas.Func (0); begin begin Result := Func_Inst (Fail_Spec_Pre); Put_Line ("ERROR 50: spec precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 50 " & Exception_Message (AE)); when others => Put_Line ("ERROR 50: unexpected exception"); end; begin Result := Func_Inst (Fail_Body_Pre); Put_Line ("ERROR 51: body precondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 51 " & Exception_Message (AE)); when others => Put_Line ("ERROR 51: unexpected exception"); end; begin Result := Func_Inst (Fail_Body_Post); Put_Line ("ERROR 52: body postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 52 " & Exception_Message (AE)); when others => Put_Line ("ERROR 52: unexpected exception"); end; begin Result := Func_Inst (Fail_Spec_Post); Put_Line ("ERROR 53: spec postcondition did not fail"); exception when AE : Assertion_Error => Put_Line ("OK 53 " & Exception_Message (AE)); when others => Put_Line ("ERROR 53: unexpected exception"); end; begin Result := Func_Inst (OK); Put_Line ("OK 54"); exception when others => Put_Line ("ERROR 54: unexpected exception"); end; end; end Main; ---------------------------- -- Compilation and output -- ---------------------------- $ gnatmake -q -gnata main.adb $ ./main OK 1 failed precondition from body_and_spec.ads:4 OK 2 failed postcondition from body_and_spec.ads:5 OK 3 OK 4 failed precondition from body_and_spec_pragmas.ads:4 OK 5 failed precondition from body_and_spec_pragmas.adb:2 OK 6 failed postcondition from body_and_spec_pragmas.adb:3 OK 7 failed postcondition from body_and_spec_pragmas.ads:5 OK 8 OK 9 failed precondition from body_only.adb:4 OK 10 failed postcondition from body_only.adb:5 OK 11 OK 12 failed precondition from body_only_pragmas.adb:2 OK 13 failed postcondition from body_only_pragmas.adb:3 OK 14 OK 15 failed precondition from gen_body_and_spec.ads:7 instantiated at main.adb:168 OK 16 failed postcondition from gen_body_and_spec.ads:8 instantiated at main.adb:168 OK 17 OK 18 failed precondition from gen_body_and_spec_pragmas.ads:7 instantiated at main.adb:201 OK 19 failed precondition from gen_body_and_spec_pragmas.adb:2 instantiated at main.adb:201 OK 20 failed postcondition from gen_body_and_spec_pragmas.adb:3 instantiated at main.adb:201 OK 21 failed postcondition from gen_body_and_spec_pragmas.ads:8 instantiated at main.adb:201 OK 22 OK 23 failed precondition from gen_pack.ads:8 instantiated at main.adb:254 OK 24 failed postcondition from gen_pack.ads:9 instantiated at main.adb:254 OK 25 OK 26 failed precondition from gen_pack_pragmas.ads:8 instantiated at main.adb:287 OK 27 failed precondition from gen_pack_pragmas.adb:3 instantiated at main.adb:287 OK 28 failed postcondition from gen_pack_pragmas.adb:4 instantiated at main.adb:287 OK 29 failed postcondition from gen_pack_pragmas.ads:9 instantiated at main.adb:287 OK 30 OK 31 failed precondition from gen_pack_gen.ads:11 instantiated at main.adb:341 OK 32 failed postcondition from gen_pack_gen.ads:12 instantiated at main.adb:341 OK 33 OK 34 failed precondition from gen_pack_gen_pragmas.ads:11 instantiated at main.adb:375 OK 35 failed precondition from gen_pack_gen_pragmas.adb:3 instantiated at main.adb:375 OK 36 failed postcondition from gen_pack_gen_pragmas.adb:4 instantiated at main.adb:375 OK 37 failed postcondition from gen_pack_gen_pragmas.ads:12 instantiated at main.adb:375 OK 38 OK 39 failed precondition from pack.ads:5 OK 40 failed postcondition from pack.ads:6 OK 41 OK 42 failed precondition from pack_pragmas.ads:5 OK 43 failed precondition from pack_pragmas.adb:3 OK 44 failed postcondition from pack_pragmas.adb:4 OK 45 failed postcondition from pack_pragmas.ads:6 OK 46 OK 47 failed precondition from pack_gen.ads:8 instantiated at main.adb:506 OK 48 failed postcondition from pack_gen.ads:9 instantiated at main.adb:506 OK 49 OK 50 failed precondition from pack_gen_pragmas.ads:8 instantiated at main.adb:539 OK 51 failed precondition from pack_gen_pragmas.adb:3 instantiated at main.adb:539 OK 52 failed postcondition from pack_gen_pragmas.adb:4 instantiated at main.adb:539 OK 53 failed postcondition from pack_gen_pragmas.ads:9 instantiated at main.adb:539 OK 54 Tested on x86_64-pc-linux-gnu, committed on trunk 2015-03-02 Hristian Kirtchev * checks.adb (Add_Validity_Check): Change the names of all formal parameters to better illustrate their purpose. Update the subprogram documentation. Update all occurrences of the formal parameters. Generate a pre/postcondition pragma by calling Build_Pre_Post_Condition. (Build_PPC_Pragma): Removed. (Build_Pre_Post_Condition): New routine. * einfo.adb Node8 is no longer used as Postcondition_Proc. Node14 is now used as Postconditions_Proc. Flag240 is now renamed to Has_Expanded_Contract. (First_Formal): The routine can now operate on generic subprograms. (First_Formal_With_Extras): The routine can now operate on generic subprograms. (Has_Expanded_Contract): New routine. (Has_Postconditions): Removed. (Postcondition_Proc): Removed. (Postconditions_Proc): New routine. (Set_Has_Expanded_Contract): New routine. (Set_Has_Postconditions): Removed. (Set_Postcondition_Proc): Removed. (Set_Postconditions_Proc): New routine. (Write_Entity_Flags): Remove the output of Has_Postconditions. Add the output of Has_Expanded_Contract. (Write_Field8_Name): Remove the output of Postcondition_Proc. (Write_Field14_Name): Add the output of Postconditions_Proc. * einfo.ads New attributes Has_Expanded_Contract and Postconditions_Proc along with occurrences in entities. Remove attributes Has_Postconditions and Postcondition_Proc along with occurrences in entities. (Has_Expanded_Contract): New routine along with pragma Inline. (Has_Postconditions): Removed along with pragma Inline. (Postcondition_Proc): Removed along with pragma Inline. (Postconditions_Proc): New routine along with pragma Inline. (Set_Has_Expanded_Contract): New routine along with pragma Inline. (Set_Has_Postconditions): Removed along with pragma Inline. (Set_Postcondition_Proc): Removed along with pragma Inline. (Set_Postconditions_Proc): New routine along with pragma Inline. * exp_ch6.adb (Add_Return): Code cleanup. Update the generation of the call to the _Postconditions routine of the procedure. (Expand_Non_Function_Return): Reformat the comment on usage. Code cleanup. Update the generation of the call to the _Postconditions routine of the procedure or entry [family]. (Expand_Simple_Function_Return): Update the generation of the _Postconditions routine of the function. (Expand_Subprogram_Contract): Reimplemented. * exp_ch6.ads (Expand_Subprogram_Contract): Update the parameter profile along the comment on usage. * exp_ch9.adb (Build_PPC_Wrapper): Code cleanup. (Expand_N_Task_Type_Declaration): Generate pre/postconditions wrapper when the entry [family] has a contract with pre/postconditions. * exp_prag.adb (Expand_Attributes_In_Consequence): New routine. (Expand_Contract_Cases): This routine and its subsidiaries now analyze all generated code. (Expand_Old_In_Consequence): Removed. * sem_attr.adb Add with and use clause for Sem_Prag. (Analyze_Attribute): Reimplment the analysis of attribute 'Result. (Check_Use_In_Test_Case): Use routine Test_Case_Arg to obtain "Ensures". * sem_ch3.adb (Analyze_Declarations): Analyze the contract of a generic subprogram. (Analyze_Object_Declaration): Do not create a contract node. (Derive_Subprogram): Do not create a contract node. * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Do not create a contract node. (Analyze_Completion_Contract): New routine. (Analyze_Function_Return): Alphabetize. (Analyze_Generic_Subprogram_Body): Alphabetize. Do not create a contract node. Do not copy pre/postconditions to the original generic template. (Analyze_Null_Procedure): Do not create a contract node. (Analyze_Subprogram_Body_Contract): Reimplemented. (Analyze_Subprogram_Body_Helper): Do not mark the enclosing scope as having postconditions. Do not create a contract node. Analyze the subprogram body contract of a body that acts as a compilation unit. Expand the subprogram contract after the declarations have been analyzed. (Analyze_Subprogram_Contract): Reimplemented. (Analyze_Subprogram_Specification): Do not create a contract node. (List_Inherited_Pre_Post_Aspects): Code cleanup. * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Update the comment on usage. (Analyze_Subprogram_Contract): Update the parameter profile and the comment on usage. * sem_ch7.adb (Analyze_Package_Body_Helper): Do not create a contract node. (Analyze_Package_Declaration): Do not create a contract node. (Is_Subp_Or_Const_Ref): Ensure that the prefix has an entity. * sem_ch8.adb (Analyze_Subprogram_Renaming): Do not create a contract node. * sem_ch9.adb (Analyze_Entry_Declaration): Do not create a contract node. * sem_ch10.adb (Analyze_Compilation_Unit): Move local variables to their proper section and alphabetize them. Analyze the contract of a [generic] subprogram after all Pragmas_After have been analyzed. (Analyze_Subprogram_Body_Stub_Contract): Alphabetize. * sem_ch12.adb (Analyze_Generic_Package_Declaration): Do not create a contract node. (Analyze_Generic_Subprogram_Declaration): Alphabetize local variables. Do not create a contract node. Do not generate aspects out of pragmas for ASIS. (Analyze_Subprogram_Instantiation): Instantiate the contract of the subprogram. Do not create a contract node. (Instantiate_Contract): New routine. (Instantiate_Subprogram_Body): Alphabetize local variables. (Save_Global_References_In_Aspects): New routine. (Save_References): Do not save the global references found within the aspects of a generic subprogram. * sem_ch12.ads (Save_Global_References_In_Aspects): New routine. * sem_ch13.adb (Analyze_Aspect_Specifications): Do not use Original_Node for establishing linkages. (Insert_Pragma): Insertion in a subprogram body takes precedence over the case where the subprogram body is also a compilation unit. * sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): Use Get_Argument to obtain the proper expression. Install the generic formals when the related context is a generic subprogram. (Analyze_Depends_In_Decl_Part): Use Get_Argument to obtain the proper expression. Use Corresponding_Spec_Of to obtain the spec. Install the generic formal when the related context is a generic subprogram. (Analyze_Global_In_Decl_Part): Use Get_Argument to obtain the proper expression. Use Corresponding_Spec_Of to obtain the spec. Install the generic formal when the related context is a generic subprogram. (Analyze_Initial_Condition_In_Decl_Part): Use Get_Argument to obtain the proper expression. Remove the call to Check_SPARK_Aspect_For_ASIS as the analysis is now done automatically. (Analyze_Pragma): Update all occurrences to Original_Aspect_Name. Pragmas Contract_Cases, Depends, Extensions_Visible, Global, Postcondition, Precondition and Test_Case now carry generic templates when the related context is a generic subprogram. The same pragmas are no longer forcefully fully analyzed when the context is a subprogram that acts as a compilation unit. Pragmas Abstract_State, Initial_Condition, Initializes and Refined_State have been clean up. Pragmas Post, Post_Class, Postcondition, Pre, Pre_Class and Precondition now use the same routine for analysis. Pragma Refined_Post does not need to check the use of 'Result or the lack of a post-state in its expression. Reimplement the analysis of pragma Test_Case. (Analyze_Pre_Post_Condition): New routine. (Analyze_Pre_Post_Condition_In_Decl_Part): Reimplemented. (Analyze_Refined_Depends_In_Decl_Part): Use Get_Argument to obtain the proper expression. (Analyze_Refined_Global_In_Decl_Part): Use Get_Argument to obtain the proper expression. (Analyze_Test_Case_In_Decl_Part): Reimplemented. (Check_Pre_Post): Removed. (Check_Precondition_Postcondition): Removed. (Check_SPARK_Aspect_For_ASIS): Removed. (Check_Test_Case): Removed. (Collect_Subprogram_Inputs_Outputs): Use Get_Argument to obtain the proper expression. Use Corresponding_Spec_Of to find the proper spec. (Create_Generic_Template): New routine. (Duplication_Error): New routine. (Expression_Function_Error): New routine. (Find_Related_Subprogram_Or_Body): Moved to the spec of Sem_Prag. Emit precise error messages. Account for cases of rewritten expression functions, generic instantiations, handled sequence of statements and pragmas from aspects. (Get_Argument): New routine. (Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed. (Preanalyze_CTC_Args): Removed. (Process_Class_Wide_Condition): New routine. * sem_prag.ads (Analyze_Test_Case_In_Decl_Part): Update the parameter profile along with the comment on usage. (Find_Related_Subprogram_Or_Body): Moved from the body of Sem_Prag. (Make_Aspect_For_PPC_In_Gen_Sub_Decl): Removed. (Test_Case_Arg): New routine. * sem_util.adb Add with and use clauses for Sem_Ch6. (Add_Contract_Item): This routine now creates a contract node the first time an item is added. Remove the duplicate aspect/pragma checks. (Check_Result_And_Post_State): Reimplemented. (Corresponding_Spec_Of): New routine. (Get_Ensures_From_CTC_Pragma): Removed. (Get_Requires_From_CTC_Pragma): Removed. (Has_Significant_Contract): New routine. (Inherit_Subprogram_Contract): Inherit only if the source has a contract. (Install_Generic_Formals): New routine. (Original_Aspect_Name): Removed. (Original_Aspect_Pragma_Name): New routine. * sem_util.ads (Check_Result_And_Post_State): Reimplemented. (Corresponding_Spec_Of): New routine. (Get_Ensures_From_CTC_Pragma): Removed. (Get_Requires_From_CTC_Pragma): Removed. (Has_Significant_Contract): New routine. (Install_Generic_Formals): New routine. (Original_Aspect_Name): Removed. (Original_Aspect_Pragma_Name): New routine. * sem_warn.adb Add with and use clauses for Sem_Prag. (Within_Postcondition): Use Test_Case_Arg to extract "Ensures". Index: exp_prag.adb =================================================================== --- exp_prag.adb (revision 221098) +++ exp_prag.adb (working copy) @@ -274,18 +274,20 @@ -- Given the entity Id of a boolean flag, generate: -- Id : Boolean := False; - procedure Expand_Old_In_Consequence + procedure Expand_Attributes_In_Consequence (Decls : List_Id; Evals : in out Node_Id; Flag : Entity_Id; Conseq : Node_Id); -- Perform specialized expansion of all attribute 'Old references found -- in consequence Conseq such that at runtime only prefixes coming from - -- the selected consequence are evaluated. Any temporaries generated in - -- the process are added to declarative list Decls. Evals is a complex - -- if statement tasked with the evaluation of all prefixes coming from - -- a selected consequence. Flag is the corresponding case guard flag. - -- Conseq is the consequence expression. + -- the selected consequence are evaluated. Similarly expand attribute + -- 'Result references by replacing them with identifier _result which + -- resolves to the sole formal parameter of procedure _Postconditions. + -- Any temporaries generated in the process are added to declarations + -- Decls. Evals is a complex if statement tasked with the evaluation of + -- all prefixes coming from a single selected consequence. Flag is the + -- corresponding case guard flag. Conseq is the consequence expression. function Increment (Id : Entity_Id) return Node_Id; -- Given the entity Id of a numerical variable, generate: @@ -409,11 +411,11 @@ Expression => New_Occurrence_Of (Standard_False, Loc)); end Declaration_Of; - ------------------------------- - -- Expand_Old_In_Consequence -- - ------------------------------- + -------------------------------------- + -- Expand_Attributes_In_Consequence -- + -------------------------------------- - procedure Expand_Old_In_Consequence + procedure Expand_Attributes_In_Consequence (Decls : List_Id; Evals : in out Node_Id; Flag : Entity_Id; @@ -423,20 +425,22 @@ -- The evaluation sequence expressed as assignment statements of all -- prefixes of attribute 'Old found in the current consequence. - function Expand_Old (N : Node_Id) return Traverse_Result; - -- Determine whether an arbitrary node denotes attribute 'Old and if - -- it does, perform all expansion-related actions. + function Expand_Attributes (N : Node_Id) return Traverse_Result; + -- Determine whether an arbitrary node denotes attribute 'Old or + -- 'Result and if it does, perform all expansion-related actions. - ---------------- - -- Expand_Old -- - ---------------- + ----------------------- + -- Expand_Attributes -- + ----------------------- - function Expand_Old (N : Node_Id) return Traverse_Result is + function Expand_Attributes (N : Node_Id) return Traverse_Result is Decl : Node_Id; Pref : Node_Id; Temp : Entity_Id; begin + -- Attribute 'Old + if Nkind (N) = N_Attribute_Reference and then Attribute_Name (N) = Name_Old then @@ -458,6 +462,7 @@ Set_No_Initialization (Decl); Prepend_To (Decls, Decl); + Analyze (Decl); -- Evaluate the prefix, generate: -- Temp := ; @@ -481,21 +486,33 @@ -- generated temporary. Rewrite (N, New_Occurrence_Of (Temp, Loc)); + + -- Attribute 'Result + + elsif Is_Attribute_Result (N) then + Rewrite (N, Make_Identifier (Loc, Name_uResult)); end if; return OK; - end Expand_Old; + end Expand_Attributes; - procedure Expand_Olds is new Traverse_Proc (Expand_Old); + procedure Expand_Attributes_In is + new Traverse_Proc (Expand_Attributes); - -- Start of processing for Expand_Old_In_Consequence + -- Start of processing for Expand_Attributes_In_Consequence begin - -- Inspect the consequence and expand any attribute 'Old references - -- found within. + -- Inspect the consequence and expand any attribute 'Old and 'Result + -- references found within. - Expand_Olds (Conseq); + Expand_Attributes_In (Conseq); + -- The consequence does not contain any attribute 'Old references + + if No (Eval_Stmts) then + return; + end if; + -- Augment the machinery to trigger the evaluation of all prefixes -- found in the step above. If Eval is empty, then this is the first -- consequence to yield expansion of 'Old. Generate: @@ -525,7 +542,7 @@ Condition => New_Occurrence_Of (Flag, Loc), Then_Statements => Eval_Stmts)); end if; - end Expand_Old_In_Consequence; + end Expand_Attributes_In_Consequence; --------------- -- Increment -- @@ -565,11 +582,15 @@ Conseq : Node_Id; Conseq_Checks : Node_Id := Empty; Count : Entity_Id; + Count_Decl : Node_Id; Error_Decls : List_Id; Flag : Entity_Id; + Flag_Decl : Node_Id; + If_Stmt : Node_Id; Msg_Str : Entity_Id; Multiple_PCs : Boolean; Old_Evals : Node_Id := Empty; + Others_Decl : Node_Id; Others_Flag : Entity_Id := Empty; Post_Case : Node_Id; @@ -596,13 +617,15 @@ -- Count : Natural := 0; Count := Make_Temporary (Loc, 'C'); - - Prepend_To (Decls, + Count_Decl := Make_Object_Declaration (Loc, Defining_Identifier => Count, Object_Definition => New_Occurrence_Of (Standard_Natural, Loc), - Expression => Make_Integer_Literal (Loc, 0))); + Expression => Make_Integer_Literal (Loc, 0)); + Prepend_To (Decls, Count_Decl); + Analyze (Count_Decl); + -- Create the base error message for multiple overlapping case guards -- Msg_Str : constant String := @@ -634,8 +657,11 @@ if Nkind (Case_Guard) = N_Others_Choice then Others_Flag := Make_Temporary (Loc, 'F'); - Prepend_To (Decls, Declaration_Of (Others_Flag)); + Others_Decl := Declaration_Of (Others_Flag); + Prepend_To (Decls, Others_Decl); + Analyze (Others_Decl); + -- Check possible overlap between a case guard and "others" if Multiple_PCs and Exception_Extra_Info then @@ -647,9 +673,9 @@ end if; -- Inspect the consequence and perform special expansion of any - -- attribute 'Old references found within. + -- attribute 'Old and 'Result references found within. - Expand_Old_In_Consequence + Expand_Attributes_In_Consequence (Decls => Decls, Evals => Old_Evals, Flag => Others_Flag, @@ -669,21 +695,27 @@ -- guard. Flag := Make_Temporary (Loc, 'F'); - Prepend_To (Decls, Declaration_Of (Flag)); + Flag_Decl := Declaration_Of (Flag); + Prepend_To (Decls, Flag_Decl); + Analyze (Flag_Decl); + -- The flag is set when the case guard is evaluated to True -- if Case_Guard then -- Flag := True; -- Count := Count + 1; -- end if; - Append_To (Decls, + If_Stmt := Make_Implicit_If_Statement (CCs, Condition => Relocate_Node (Case_Guard), Then_Statements => New_List ( Set (Flag), - Increment (Count)))); + Increment (Count))); + Append_To (Decls, If_Stmt); + Analyze (If_Stmt); + -- Check whether this case guard overlaps with another one if Multiple_PCs and Exception_Extra_Info then @@ -695,9 +727,9 @@ end if; -- Inspect the consequence and perform special expansion of any - -- attribute 'Old references found within. + -- attribute 'Old and 'Result references found within. - Expand_Old_In_Consequence + Expand_Attributes_In_Consequence (Decls => Decls, Evals => Old_Evals, Flag => Flag, @@ -783,11 +815,15 @@ end if; Append_To (Decls, CG_Checks); + Analyze (CG_Checks); -- Once all case guards are evaluated and checked, evaluate any prefixes -- of attribute 'Old founds in the selected consequence. - Append_To (Decls, Old_Evals); + if Present (Old_Evals) then + Append_To (Decls, Old_Evals); + Analyze (Old_Evals); + end if; -- Raise Assertion_Error when the corresponding consequence of a case -- guard that evaluated to True fails. Index: sem_ch3.adb =================================================================== --- sem_ch3.adb (revision 221098) +++ sem_ch3.adb (working copy) @@ -2471,6 +2471,7 @@ Analyze_Object_Contract (Defining_Entity (Decl)); elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration, + N_Generic_Subprogram_Declaration, N_Subprogram_Declaration) then Analyze_Subprogram_Contract (Defining_Entity (Decl)); @@ -4116,8 +4117,6 @@ if Present (E) then Set_Has_Initial_Value (Id); end if; - - Set_Contract (Id, Make_Contract (Sloc (Id))); end if; -- Initialize alignment and size and capture alignment setting @@ -14486,7 +14485,6 @@ begin New_Subp := New_Entity (Nkind (Parent_Subp), Sloc (Derived_Type)); Set_Ekind (New_Subp, Ekind (Parent_Subp)); - Set_Contract (New_Subp, Make_Contract (Sloc (New_Subp))); -- Check whether the inherited subprogram is a private operation that -- should be inherited but not yet made visible. Such subprograms can @@ -16468,7 +16466,7 @@ Set_Has_Private_Declaration (Prev); Set_Has_Private_Declaration (Id); - -- AI12-0133: Indicate whether we have a partial view with + -- AI12-0133: indicate whether we have a partial view with -- unknown discriminants, in which case initialization of objects -- of the type do not receive an invariant check. @@ -19445,7 +19443,7 @@ and then Limited_Present (Type_Definition (Orig_Decl)) then Error_Msg_N - ("full view of non-limited extension cannot be limited", N); + ("full view of non-limited extension cannot be limited", N); -- Conversely, if the partial view carries the limited keyword, -- the full view must as well, even if it may be redundant. @@ -19454,8 +19452,8 @@ and then not Limited_Present (Type_Definition (Orig_Decl)) then Error_Msg_N - ("full view of limited extension must be explicitly limited", - N); + ("full view of limited extension must be explicitly limited", + N); end if; end if; end; Index: exp_ch9.adb =================================================================== --- exp_ch9.adb (revision 221098) +++ exp_ch9.adb (working copy) @@ -1919,68 +1919,59 @@ ----------------------- procedure Build_PPC_Wrapper (E : Entity_Id; Decl : Node_Id) is + Items : constant Node_Id := Contract (E); Loc : constant Source_Ptr := Sloc (E); - Synch_Type : constant Entity_Id := Scope (E); - - Wrapper_Id : constant Entity_Id := - Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (E), 'E')); - -- the wrapper procedure name - - Wrapper_Body : Node_Id; - - Synch_Id : constant Entity_Id := - Make_Defining_Identifier (Loc, - Chars => New_External_Name (Chars (Scope (E)), 'A')); - -- The parameter that designates the synchronized object in the call - - Actuals : constant List_Id := New_List; - -- The actuals in the entry call - - Decls : constant List_Id := New_List; - + Synch_Type : constant Entity_Id := Scope (E); + Actuals : List_Id; + Decls : List_Id; Entry_Call : Node_Id; Entry_Name : Node_Id; + Params : List_Id; + Prag : Node_Id; + Synch_Id : Entity_Id; + Wrapper_Id : Entity_Id; - Specs : List_Id; - -- The specification of the wrapper procedure - begin - - -- Only build the wrapper if entry has pre/postconditions. + -- Only build the wrapper if entry has pre/postconditions -- Should this be done unconditionally instead ??? - declare - P : Node_Id; + if Present (Items) then + Prag := Pre_Post_Conditions (Items); - begin - P := Pre_Post_Conditions (Contract (E)); - - if No (P) then + if No (Prag) then return; end if; -- Transfer ppc pragmas to the declarations of the wrapper - while Present (P) loop - if Nam_In (Pragma_Name (P), Name_Precondition, - Name_Postcondition) + Decls := New_List; + + while Present (Prag) loop + if Nam_In (Pragma_Name (Prag), Name_Precondition, + Name_Postcondition) then - Append (Relocate_Node (P), Decls); + Append (Relocate_Node (Prag), Decls); Set_Analyzed (Last (Decls), False); end if; - P := Next_Pragma (P); + Prag := Next_Pragma (Prag); end loop; - end; + else + return; + end if; + Actuals := New_List; + Synch_Id := + Make_Defining_Identifier (Loc, + Chars => New_External_Name (Chars (Scope (E)), 'A')); + -- First formal is synchronized object - Specs := New_List ( + Params := New_List ( Make_Parameter_Specification (Loc, Defining_Identifier => Synch_Id, - Out_Present => True, - In_Present => True, + Out_Present => True, + In_Present => True, Parameter_Type => New_Occurrence_Of (Scope (E), Loc))); Entry_Name := @@ -1996,7 +1987,7 @@ Index : constant Entity_Id := Make_Defining_Identifier (Loc, Name_I); begin - Append_To (Specs, + Append_To (Params, Make_Parameter_Specification (Loc, Defining_Identifier => Index, Parameter_Type => @@ -2033,7 +2024,7 @@ In_Present => In_Present (Parent (Form)), Parameter_Type => New_Occurrence_Of (Etype (Form), Loc)); - Append (Parm_Spec, Specs); + Append (Parm_Spec, Params); Append (New_Occurrence_Of (New_Form, Loc), Actuals); Next_Formal (Form); end loop; @@ -2065,21 +2056,22 @@ end; end if; + Wrapper_Id := + Make_Defining_Identifier (Loc, New_External_Name (Chars (E), 'E')); Set_PPC_Wrapper (E, Wrapper_Id); - Wrapper_Body := + + -- The wrapper body is analyzed when the enclosing type is frozen + + Append_Freeze_Action (Defining_Entity (Decl), Make_Subprogram_Body (Loc, Specification => Make_Procedure_Specification (Loc, Defining_Unit_Name => Wrapper_Id, - Parameter_Specifications => Specs), + Parameter_Specifications => Params), Declarations => Decls, Handled_Statement_Sequence => Make_Handled_Sequence_Of_Statements (Loc, - Statements => New_List (Entry_Call))); - - -- The wrapper body is analyzed when the enclosing type is frozen - - Append_Freeze_Action (Defining_Entity (Decl), Wrapper_Body); + Statements => New_List (Entry_Call)))); end Build_PPC_Wrapper; -------------------------- @@ -12087,6 +12079,7 @@ Ent := First_Entity (Tasktyp); while Present (Ent) loop if Ekind_In (Ent, E_Entry, E_Entry_Family) + and then Present (Contract (Ent)) and then Present (Pre_Post_Conditions (Contract (Ent))) then Build_PPC_Wrapper (Ent, N); Index: sem_ch7.adb =================================================================== --- sem_ch7.adb (revision 221098) +++ sem_ch7.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -297,6 +297,7 @@ elsif Nkind (N) = N_Attribute_Reference and then Is_Entity_Name (Prefix (N)) + and then Present (Entity (Prefix (N))) and then Is_Subprogram (Entity (Prefix (N))) then Reference_Seen := True; @@ -690,7 +691,6 @@ Set_Ekind (Body_Id, E_Package_Body); Set_Body_Entity (Spec_Id, Body_Id); Set_Spec_Entity (Body_Id, Spec_Id); - Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); -- Defining name for the package body is not a visible entity: Only the -- defining name for the declaration is visible. @@ -1017,9 +1017,8 @@ Generate_Definition (Id); Enter_Name (Id); - Set_Ekind (Id, E_Package); - Set_Etype (Id, Standard_Void_Type); - Set_Contract (Id, Make_Contract (Sloc (Id))); + Set_Ekind (Id, E_Package); + Set_Etype (Id, Standard_Void_Type); -- Set SPARK_Mode from context only for non-generic package Index: sem_ch9.adb =================================================================== --- sem_ch9.adb (revision 221098) +++ sem_ch9.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -1496,7 +1496,7 @@ begin Generate_Definition (Def_Id); - Set_Contract (Def_Id, Make_Contract (Sloc (Def_Id))); + Tasking_Used := True; -- Case of no discrete subtype definition Index: sem_ch10.adb =================================================================== --- sem_ch10.adb (revision 221098) +++ sem_ch10.adb (working copy) @@ -246,13 +246,6 @@ ------------------------------ procedure Analyze_Compilation_Unit (N : Node_Id) is - Unit_Node : constant Node_Id := Unit (N); - Lib_Unit : Node_Id := Library_Unit (N); - Spec_Id : Entity_Id; - Main_Cunit : constant Node_Id := Cunit (Main_Unit); - Par_Spec_Name : Unit_Name_Type; - Unum : Unit_Number_Type; - procedure Check_Redundant_Withs (Context_Items : List_Id; Spec_Context_Items : List_Id := No_List); @@ -602,6 +595,15 @@ end loop; end Check_Redundant_Withs; + -- Local variables + + Main_Cunit : constant Node_Id := Cunit (Main_Unit); + Unit_Node : constant Node_Id := Unit (N); + Lib_Unit : Node_Id := Library_Unit (N); + Par_Spec_Name : Unit_Name_Type; + Spec_Id : Entity_Id; + Unum : Unit_Number_Type; + -- Start of processing for Analyze_Compilation_Unit begin @@ -930,6 +932,15 @@ end; end if; + -- Analyze the contract of a [generic] subprogram that acts as a + -- compilation unit after all compilation pragmas have been analyzed. + + if Nkind_In (Unit_Node, N_Generic_Subprogram_Declaration, + N_Subprogram_Declaration) + then + Analyze_Subprogram_Contract (Defining_Entity (Unit_Node)); + end if; + -- Generate distribution stubs if requested and no error if N = Main_Cunit @@ -1920,39 +1931,6 @@ end if; end Analyze_Protected_Body_Stub; - ------------------------------------------- - -- Analyze_Subprogram_Body_Stub_Contract -- - ------------------------------------------- - - procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is - Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); - Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); - - begin - -- A subprogram body stub may act as its own spec or as the completion - -- of a previous declaration. Depending on the context, the contract of - -- the stub may contain two sets of pragmas. - - -- The stub is a completion, the applicable pragmas are: - -- Contract_Cases - -- Depends - -- Global - -- Postcondition - -- Precondition - -- Test_Case - - if Present (Spec_Id) then - Analyze_Subprogram_Body_Contract (Stub_Id); - - -- The stub acts as its own spec, the applicable pragmas are: - -- Refined_Depends - -- Refined_Global - - else - Analyze_Subprogram_Contract (Stub_Id); - end if; - end Analyze_Subprogram_Body_Stub_Contract; - ---------------------------------- -- Analyze_Subprogram_Body_Stub -- ---------------------------------- @@ -2005,6 +1983,39 @@ Restore_Opt_Config_Switches (Opts); end Analyze_Subprogram_Body_Stub; + ------------------------------------------- + -- Analyze_Subprogram_Body_Stub_Contract -- + ------------------------------------------- + + procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is + Stub_Decl : constant Node_Id := Parent (Parent (Stub_Id)); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl); + + begin + -- A subprogram body stub may act as its own spec or as the completion + -- of a previous declaration. Depending on the context, the contract of + -- the stub may contain two sets of pragmas. + + -- The stub is a completion, the applicable pragmas are: + -- Refined_Depends + -- Refined_Global + + if Present (Spec_Id) then + Analyze_Subprogram_Body_Contract (Stub_Id); + + -- The stub acts as its own spec, the applicable pragmas are: + -- Contract_Cases + -- Depends + -- Global + -- Postcondition + -- Precondition + -- Test_Case + + else + Analyze_Subprogram_Contract (Stub_Id); + end if; + end Analyze_Subprogram_Body_Stub_Contract; + --------------------- -- Analyze_Subunit -- --------------------- @@ -2831,13 +2842,13 @@ when None => null; - -- If with'ed unit had a detected fatal error, propagate it + -- If with'ed unit had a detected fatal error, propagate it when Error_Detected => Set_Fatal_Error (Current_Sem_Unit, Error_Detected); - -- If with'ed unit had an ignored error, then propagate it - -- but do not overide an existring setting. + -- If with'ed unit had an ignored error, then propagate it but do not + -- overide an existring setting. when Error_Ignored => if Fatal_Error (Current_Sem_Unit) = None then Index: einfo.adb =================================================================== --- einfo.adb (revision 221098) +++ einfo.adb (working copy) @@ -79,7 +79,6 @@ -- Hiding_Loop_Variable Node8 -- Mechanism Uint8 (but returns Mechanism_Type) -- Normalized_First_Bit Uint8 - -- Postcondition_Proc Node8 -- Refinement_Constituents Elist8 -- Return_Applies_To Node8 -- First_Exit_Statement Node8 @@ -116,6 +115,7 @@ -- Alignment Uint14 -- Normalized_Position Uint14 + -- Postconditions_Proc Node14 -- Shadow_Entities List14 -- Discriminant_Number Uint15 @@ -532,7 +532,7 @@ -- Warnings_Off_Used_Unmodified Flag237 -- Warnings_Off_Used_Unreferenced Flag238 -- OK_To_Reorder_Components Flag239 - -- Has_Postconditions Flag240 + -- Has_Expanded_Contract Flag240 -- Optimize_Alignment_Space Flag241 -- Optimize_Alignment_Time Flag242 @@ -1456,6 +1456,12 @@ return Flag47 (Id); end Has_Exit; + function Has_Expanded_Contract (Id : E) return B is + begin + pragma Assert (Is_Subprogram (Id)); + return Flag240 (Id); + end Has_Expanded_Contract; + function Has_Forward_Instantiation (Id : E) return B is begin return Flag175 (Id); @@ -1560,12 +1566,6 @@ return Flag154 (Id); end Has_Per_Object_Constraint; - function Has_Postconditions (Id : E) return B is - begin - pragma Assert (Is_Subprogram (Id)); - return Flag240 (Id); - end Has_Postconditions; - function Has_Pragma_Controlled (Id : E) return B is begin pragma Assert (Is_Access_Type (Id)); @@ -2750,11 +2750,14 @@ return Elist15 (Id); end Pending_Access_Types; - function Postcondition_Proc (Id : E) return E is + function Postconditions_Proc (Id : E) return E is begin - pragma Assert (Ekind (Id) = E_Procedure); - return Node8 (Id); - end Postcondition_Proc; + pragma Assert (Ekind_In (Id, E_Entry, + E_Entry_Family, + E_Function, + E_Procedure)); + return Node14 (Id); + end Postconditions_Proc; function PPC_Wrapper (Id : E) return E is begin @@ -4276,6 +4279,15 @@ Set_Flag47 (Id, V); end Set_Has_Exit; + procedure Set_Has_Expanded_Contract (Id : E; V : B := True) is + begin + pragma Assert (Ekind_In (Id, E_Entry, + E_Entry_Family, + E_Function, + E_Procedure)); + Set_Flag240 (Id, V); + end Set_Has_Expanded_Contract; + procedure Set_Has_Forward_Instantiation (Id : E; V : B := True) is begin Set_Flag175 (Id, V); @@ -4388,12 +4400,6 @@ Set_Flag154 (Id, V); end Set_Has_Per_Object_Constraint; - procedure Set_Has_Postconditions (Id : E; V : B := True) is - begin - pragma Assert (Is_Subprogram (Id)); - Set_Flag240 (Id, V); - end Set_Has_Postconditions; - procedure Set_Has_Pragma_Controlled (Id : E; V : B := True) is begin pragma Assert (Is_Access_Type (Id)); @@ -5649,11 +5655,14 @@ Set_Elist15 (Id, V); end Set_Pending_Access_Types; - procedure Set_Postcondition_Proc (Id : E; V : E) is + procedure Set_Postconditions_Proc (Id : E; V : E) is begin - pragma Assert (Ekind (Id) = E_Procedure); - Set_Node8 (Id, V); - end Set_Postcondition_Proc; + pragma Assert (Ekind_In (Id, E_Entry, + E_Entry_Family, + E_Function, + E_Procedure)); + Set_Node14 (Id, V); + end Set_Postconditions_Proc; procedure Set_PPC_Wrapper (Id : E; V : E) is begin @@ -6685,7 +6694,8 @@ begin pragma Assert - (Is_Overloadable (Id) + (Is_Generic_Subprogram (Id) + or else Is_Overloadable (Id) or else Ekind_In (Id, E_Entry_Family, E_Subprogram_Body, E_Subprogram_Type)); @@ -6696,6 +6706,16 @@ else Formal := First_Entity (Id); + -- The first/next entity chain of a generic subprogram contains all + -- generic formal parameters, followed by the formal parameters. Go + -- directly to the paramters by skipping the formal part. + + if Is_Generic_Subprogram (Id) then + while Present (Formal) and then not Is_Formal (Formal) loop + Next_Entity (Formal); + end loop; + end if; + if Present (Formal) and then Is_Formal (Formal) then return Formal; else @@ -6713,7 +6733,8 @@ begin pragma Assert - (Is_Overloadable (Id) + (Is_Generic_Subprogram (Id) + or else Is_Overloadable (Id) or else Ekind_In (Id, E_Entry_Family, E_Subprogram_Body, E_Subprogram_Type)); @@ -6724,6 +6745,16 @@ else Formal := First_Entity (Id); + -- The first/next entity chain of a generic subprogram contains all + -- generic formal parameters, followed by the formal parameters. Go + -- directly to the paramters by skipping the formal part. + + if Is_Generic_Subprogram (Id) then + while Present (Formal) and then not Is_Formal (Formal) loop + Next_Entity (Formal); + end loop; + end if; + if Present (Formal) and then Is_Formal (Formal) then return Formal; else @@ -8470,6 +8501,7 @@ W ("Has_Dynamic_Predicate_Aspect", Flag258 (Id)); W ("Has_Enumeration_Rep_Clause", Flag66 (Id)); W ("Has_Exit", Flag47 (Id)); + W ("Has_Expanded_Contract", Flag240 (Id)); W ("Has_Forward_Instantiation", Flag175 (Id)); W ("Has_Fully_Qualified_Name", Flag173 (Id)); W ("Has_Gigi_Rep_Item", Flag82 (Id)); @@ -8489,7 +8521,6 @@ W ("Has_Out_Or_In_Out_Parameter", Flag110 (Id)); W ("Has_Object_Size_Clause", Flag172 (Id)); W ("Has_Per_Object_Constraint", Flag154 (Id)); - W ("Has_Postconditions", Flag240 (Id)); W ("Has_Pragma_Controlled", Flag27 (Id)); W ("Has_Pragma_Elaborate_Body", Flag150 (Id)); W ("Has_Pragma_Inline", Flag157 (Id)); @@ -8882,9 +8913,6 @@ E_Discriminant => Write_Str ("Normalized_First_Bit"); - when E_Procedure => - Write_Str ("Postcondition_Proc"); - when E_Abstract_State => Write_Str ("Refinement_Constituents"); @@ -9083,16 +9111,22 @@ Formal_Kind | E_Constant | E_Exception | - E_Variable | - E_Loop_Parameter => + E_Loop_Parameter | + E_Variable => Write_Str ("Alignment"); when E_Component | E_Discriminant => Write_Str ("Normalized_Position"); - when E_Package | - E_Generic_Package => + when E_Entry | + E_Entry_Family | + E_Function | + E_Procedure => + Write_Str ("Postconditions_Proc"); + + when E_Generic_Package | + E_Package => Write_Str ("Shadow_Entities"); when others => Index: einfo.ads =================================================================== --- einfo.ads (revision 221098) +++ einfo.ads (working copy) @@ -1565,6 +1565,12 @@ -- Has_Exit (Flag47) -- Defined in loop entities. Set if the loop contains an exit statement. +-- Has_Expanded_Contract (Flag240) +-- Defined in functions, procedures, entries, and entry families. Set +-- when a subprogram has a N_Contract node that has been expanded. The +-- flag prevents double expansion of a contract when a construct is +-- rewritten into something else and subsequently reanalyzed/expanded. + -- Has_Foreign_Convention (synthesized) -- Applies to all entities. Determines if the Convention for the -- entity is a foreign convention (i.e. is other than Convention_Ada, @@ -1734,10 +1740,6 @@ -- 5. N_Range_Constraint - when the range expression uses the -- discriminant of the enclosing type. --- Has_Postconditions (Flag240) --- Defined in subprogram entities. Set if postconditions are active for --- the procedure, and a _postconditions procedure has been generated. - -- Has_Pragma_Controlled (Flag27) [implementation base type only] -- Defined in access type entities. It is set if a pragma Controlled -- applies to the access type. @@ -3591,11 +3593,10 @@ -- ensure that the finalization masters of all pending access types are -- fully initialized when the full view is frozen. --- Postcondition_Proc (Node8) --- Defined only in procedure entities, saves the entity of the generated --- postcondition proc if one is present, otherwise is set to Empty. Used --- to generate the call to this procedure in case the expander inserts --- implicit return statements. +-- Postconditions_Proc (Node14) +-- Defined in functions, procedures, entries, and entry families. Refers +-- to the entity of the _Postconditions procedure used to check contract +-- assertions on exit from a subprogram. -- PPC_Wrapper (Node25) -- Defined in entries and entry families. Set only if pre- or post- @@ -5611,6 +5612,7 @@ -- E_Entry_Family -- Protected_Body_Subprogram (Node11) -- Barrier_Function (Node12) + -- Postconditions_Proc (Node14) -- Entry_Parameters_Type (Node15) -- First_Entity (Node17) -- Alias (Node18) (for entry only. Empty) @@ -5621,11 +5623,12 @@ -- PPC_Wrapper (Node25) -- Extra_Formals (Node28) -- Contract (Node34) + -- Needs_No_Actuals (Flag22) + -- Uses_Sec_Stack (Flag95) -- Default_Expressions_Processed (Flag108) -- Entry_Accepted (Flag152) - -- Needs_No_Actuals (Flag22) -- Sec_Stack_Needed_For_Return (Flag167) - -- Uses_Sec_Stack (Flag95) + -- Has_Expanded_Contract (Flag240) -- Address_Clause (synth) -- Entry_Index_Type (synth) -- First_Formal (synth) @@ -5707,6 +5710,7 @@ -- Protected_Body_Subprogram (Node11) -- Next_Inlined_Subprogram (Node12) -- Elaboration_Entity (Node13) (not implicit /=) + -- Postconditions_Proc (Node14) (non-generic case only) -- DT_Position (Uint15) -- DTC_Entity (Node16) -- First_Entity (Node17) @@ -5739,12 +5743,12 @@ -- Has_Anonymous_Master (Flag253) -- Has_Completion (Flag26) -- Has_Controlling_Result (Flag98) + -- Has_Expanded_Contract (Flag240) (non-generic case only) -- Has_Invariants (Flag232) -- Has_Master_Entity (Flag21) -- Has_Missing_Return (Flag142) -- Has_Nested_Block_With_Handler (Flag101) -- Has_Out_Or_In_Out_Parameter (Flag110) - -- Has_Postconditions (Flag240) -- Has_Recursive_Call (Flag143) -- Is_Abstract_Subprogram (Flag19) (non-generic case only) -- Is_Called (Flag102) (non-generic case only) @@ -5892,7 +5896,6 @@ -- Linker_Section_Pragma (Node33) -- Contract (Node34) -- Has_Invariants (Flag232) - -- Has_Postconditions (Flag240) -- Is_Machine_Code_Subprogram (Flag137) -- Is_Pure (Flag44) -- Is_Intrinsic_Subprogram (Flag64) @@ -6002,12 +6005,12 @@ -- E_Procedure -- E_Generic_Procedure - -- Postcondition_Proc (Node8) (non-generic case only) -- Renaming_Map (Uint9) -- Handler_Records (List10) (non-generic case only) -- Protected_Body_Subprogram (Node11) -- Next_Inlined_Subprogram (Node12) -- Elaboration_Entity (Node13) + -- Postconditions_Proc (Node14) (non-generic case only) -- DT_Position (Uint15) -- DTC_Entity (Node16) -- First_Entity (Node17) @@ -6039,10 +6042,10 @@ -- Discard_Names (Flag88) -- Has_Anonymous_Master (Flag253) -- Has_Completion (Flag26) + -- Has_Expanded_Contract (Flag240) (non-generic case only) -- Has_Invariants (Flag232) -- Has_Master_Entity (Flag21) -- Has_Nested_Block_With_Handler (Flag101) - -- Has_Postconditions (Flag240) -- Is_Abstract_Subprogram (Flag19) (non-generic case only) -- Is_Asynchronous (Flag81) -- Is_Called (Flag102) (non-generic case only) @@ -6656,6 +6659,7 @@ function Has_Dynamic_Predicate_Aspect (Id : E) return B; function Has_Enumeration_Rep_Clause (Id : E) return B; function Has_Exit (Id : E) return B; + function Has_Expanded_Contract (Id : E) return B; function Has_Forward_Instantiation (Id : E) return B; function Has_Fully_Qualified_Name (Id : E) return B; function Has_Gigi_Rep_Item (Id : E) return B; @@ -6676,7 +6680,6 @@ function Has_Object_Size_Clause (Id : E) return B; function Has_Out_Or_In_Out_Parameter (Id : E) return B; function Has_Per_Object_Constraint (Id : E) return B; - function Has_Postconditions (Id : E) return B; function Has_Pragma_Controlled (Id : E) return B; function Has_Pragma_Elaborate_Body (Id : E) return B; function Has_Pragma_Inline (Id : E) return B; @@ -6885,7 +6888,7 @@ function Part_Of_Constituents (Id : E) return L; function Partial_View_Has_Unknown_Discr (Id : E) return B; function Pending_Access_Types (Id : E) return L; - function Postcondition_Proc (Id : E) return E; + function Postconditions_Proc (Id : E) return E; function Prival (Id : E) return E; function Prival_Link (Id : E) return E; function Private_Dependents (Id : E) return L; @@ -7299,6 +7302,7 @@ procedure Set_Has_Dynamic_Predicate_Aspect (Id : E; V : B := True); procedure Set_Has_Enumeration_Rep_Clause (Id : E; V : B := True); procedure Set_Has_Exit (Id : E; V : B := True); + procedure Set_Has_Expanded_Contract (Id : E; V : B := True); procedure Set_Has_Forward_Instantiation (Id : E; V : B := True); procedure Set_Has_Fully_Qualified_Name (Id : E; V : B := True); procedure Set_Has_Gigi_Rep_Item (Id : E; V : B := True); @@ -7318,7 +7322,6 @@ procedure Set_Has_Object_Size_Clause (Id : E; V : B := True); procedure Set_Has_Out_Or_In_Out_Parameter (Id : E; V : B := True); procedure Set_Has_Per_Object_Constraint (Id : E; V : B := True); - procedure Set_Has_Postconditions (Id : E; V : B := True); procedure Set_Has_Pragma_Controlled (Id : E; V : B := True); procedure Set_Has_Pragma_Elaborate_Body (Id : E; V : B := True); procedure Set_Has_Pragma_Inline (Id : E; V : B := True); @@ -7533,7 +7536,7 @@ procedure Set_Part_Of_Constituents (Id : E; V : L); procedure Set_Partial_View_Has_Unknown_Discr (Id : E; V : B := True); procedure Set_Pending_Access_Types (Id : E; V : L); - procedure Set_Postcondition_Proc (Id : E; V : E); + procedure Set_Postconditions_Proc (Id : E; V : E); procedure Set_Prival (Id : E; V : E); procedure Set_Prival_Link (Id : E; V : E); procedure Set_Private_Dependents (Id : E; V : L); @@ -8057,6 +8060,7 @@ pragma Inline (Has_Dynamic_Predicate_Aspect); pragma Inline (Has_Enumeration_Rep_Clause); pragma Inline (Has_Exit); + pragma Inline (Has_Expanded_Contract); pragma Inline (Has_Forward_Instantiation); pragma Inline (Has_Fully_Qualified_Name); pragma Inline (Has_Gigi_Rep_Item); @@ -8076,7 +8080,6 @@ pragma Inline (Has_Object_Size_Clause); pragma Inline (Has_Out_Or_In_Out_Parameter); pragma Inline (Has_Per_Object_Constraint); - pragma Inline (Has_Postconditions); pragma Inline (Has_Pragma_Controlled); pragma Inline (Has_Pragma_Elaborate_Body); pragma Inline (Has_Pragma_Inline); @@ -8333,7 +8336,7 @@ pragma Inline (Part_Of_Constituents); pragma Inline (Partial_View_Has_Unknown_Discr); pragma Inline (Pending_Access_Types); - pragma Inline (Postcondition_Proc); + pragma Inline (Postconditions_Proc); pragma Inline (Prival); pragma Inline (Prival_Link); pragma Inline (Private_Dependents); @@ -8547,6 +8550,7 @@ pragma Inline (Set_Has_Dynamic_Predicate_Aspect); pragma Inline (Set_Has_Enumeration_Rep_Clause); pragma Inline (Set_Has_Exit); + pragma Inline (Set_Has_Expanded_Contract); pragma Inline (Set_Has_Forward_Instantiation); pragma Inline (Set_Has_Fully_Qualified_Name); pragma Inline (Set_Has_Gigi_Rep_Item); @@ -8566,7 +8570,6 @@ pragma Inline (Set_Has_Object_Size_Clause); pragma Inline (Set_Has_Out_Or_In_Out_Parameter); pragma Inline (Set_Has_Per_Object_Constraint); - pragma Inline (Set_Has_Postconditions); pragma Inline (Set_Has_Pragma_Controlled); pragma Inline (Set_Has_Pragma_Elaborate_Body); pragma Inline (Set_Has_Pragma_Inline); @@ -8780,7 +8783,7 @@ pragma Inline (Set_Part_Of_Constituents); pragma Inline (Set_Partial_View_Has_Unknown_Discr); pragma Inline (Set_Pending_Access_Types); - pragma Inline (Set_Postcondition_Proc); + pragma Inline (Set_Postconditions_Proc); pragma Inline (Set_Prival); pragma Inline (Set_Prival_Link); pragma Inline (Set_Private_Dependents); Index: checks.adb =================================================================== --- checks.adb (revision 221098) +++ checks.adb (working copy) @@ -2417,31 +2417,95 @@ Subp_Decl : Node_Id; procedure Add_Validity_Check - (Context : Entity_Id; - PPC_Nam : Name_Id; + (Formal : Entity_Id; + Prag_Nam : Name_Id; For_Result : Boolean := False); -- Add a single 'Valid[_Scalar] check which verifies the initialization - -- of Context. PPC_Nam denotes the pre or post condition pragma name. + -- of Formal. Prag_Nam denotes the pre or post condition pragma name. -- Set flag For_Result when to verify the result of a function. - procedure Build_PPC_Pragma (PPC_Nam : Name_Id; Check : Node_Id); - -- Create a pre or post condition pragma with name PPC_Nam which - -- tests expression Check. - ------------------------ -- Add_Validity_Check -- ------------------------ procedure Add_Validity_Check - (Context : Entity_Id; - PPC_Nam : Name_Id; + (Formal : Entity_Id; + Prag_Nam : Name_Id; For_Result : Boolean := False) is + procedure Build_Pre_Post_Condition (Expr : Node_Id); + -- Create a pre/postcondition pragma that tests expression Expr + + ------------------------------ + -- Build_Pre_Post_Condition -- + ------------------------------ + + procedure Build_Pre_Post_Condition (Expr : Node_Id) is + Loc : constant Source_Ptr := Sloc (Subp); + Decls : List_Id; + Prag : Node_Id; + + begin + Prag := + Make_Pragma (Loc, + Pragma_Identifier => + Make_Identifier (Loc, Prag_Nam), + Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Chars => Name_Check, + Expression => Expr))); + + -- Add a message unless exception messages are suppressed + + if not Exception_Locations_Suppressed then + Append_To (Pragma_Argument_Associations (Prag), + Make_Pragma_Argument_Association (Loc, + Chars => Name_Message, + Expression => + Make_String_Literal (Loc, + Strval => "failed " + & Get_Name_String (Prag_Nam) + & " from " + & Build_Location_String (Loc)))); + end if; + + -- Insert the pragma in the tree + + if Nkind (Parent (Subp_Decl)) = N_Compilation_Unit then + Add_Global_Declaration (Prag); + Analyze (Prag); + + -- PPC pragmas associated with subprogram bodies must be inserted + -- in the declarative part of the body. + + elsif Nkind (Subp_Decl) = N_Subprogram_Body then + Decls := Declarations (Subp_Decl); + + if No (Decls) then + Decls := New_List; + Set_Declarations (Subp_Decl, Decls); + end if; + + Prepend_To (Decls, Prag); + Analyze (Prag); + + -- For subprogram declarations insert the PPC pragma right after + -- the declarative node. + + else + Insert_After_And_Analyze (Subp_Decl, Prag); + end if; + end Build_Pre_Post_Condition; + + -- Local variables + Loc : constant Source_Ptr := Sloc (Subp); - Typ : constant Entity_Id := Etype (Context); + Typ : constant Entity_Id := Etype (Formal); Check : Node_Id; Nam : Name_Id; + -- Start of processing for Add_Validity_Check + begin -- For scalars, generate 'Valid test @@ -2462,7 +2526,7 @@ -- Step 1: Create the expression to verify the validity of the -- context. - Check := New_Occurrence_Of (Context, Loc); + Check := New_Occurrence_Of (Formal, Loc); -- When processing a function result, use 'Result. Generate -- Context'Result @@ -2484,73 +2548,9 @@ -- Step 2: Create a pre or post condition pragma - Build_PPC_Pragma (PPC_Nam, Check); + Build_Pre_Post_Condition (Check); end Add_Validity_Check; - ---------------------- - -- Build_PPC_Pragma -- - ---------------------- - - procedure Build_PPC_Pragma (PPC_Nam : Name_Id; Check : Node_Id) is - Loc : constant Source_Ptr := Sloc (Subp); - Decls : List_Id; - Prag : Node_Id; - - begin - Prag := - Make_Pragma (Loc, - Pragma_Identifier => Make_Identifier (Loc, PPC_Nam), - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Chars => Name_Check, - Expression => Check))); - - -- Add a message unless exception messages are suppressed - - if not Exception_Locations_Suppressed then - Append_To (Pragma_Argument_Associations (Prag), - Make_Pragma_Argument_Association (Loc, - Chars => Name_Message, - Expression => - Make_String_Literal (Loc, - Strval => "failed " & Get_Name_String (PPC_Nam) & - " from " & Build_Location_String (Loc)))); - end if; - - -- Insert the pragma in the tree - - if Nkind (Parent (Subp_Decl)) = N_Compilation_Unit then - Add_Global_Declaration (Prag); - Analyze (Prag); - - -- PPC pragmas associated with subprogram bodies must be inserted in - -- the declarative part of the body. - - elsif Nkind (Subp_Decl) = N_Subprogram_Body then - Decls := Declarations (Subp_Decl); - - if No (Decls) then - Decls := New_List; - Set_Declarations (Subp_Decl, Decls); - end if; - - Prepend_To (Decls, Prag); - - -- Ensure the proper visibility of the subprogram body and its - -- parameters. - - Push_Scope (Subp); - Analyze (Prag); - Pop_Scope; - - -- For subprogram declarations insert the PPC pragma right after the - -- declarative node. - - else - Insert_After_And_Analyze (Subp_Decl, Prag); - end if; - end Build_PPC_Pragma; - -- Local variables Formal : Entity_Id; Index: sem_prag.adb =================================================================== --- sem_prag.adb (revision 221098) +++ sem_prag.adb (working copy) @@ -202,12 +202,6 @@ -- _Post, _Invariant, or _Type_Invariant, which are special names used -- in identifiers to represent these attribute references. - procedure Check_SPARK_Aspect_For_ASIS (N : Node_Id); - -- In ASIS mode we need to analyze the original expression in the aspect - -- specification. For Initializes, Global, and related SPARK aspects, the - -- expression has a sui-generis syntax which may be a list, an expression, - -- or an aggregate. - procedure Check_State_And_Constituent_Use (States : Elist_Id; Constits : Elist_Id; @@ -217,22 +211,34 @@ -- corresponding constituent from list Constits (if any) appear in the same -- context denoted by Context. If this is the case, emit an error. - function Find_Related_Subprogram_Or_Body + procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id); + -- Subsidiary to routines Find_Related_Package_Or_Body and + -- Find_Related_Subprogram_Or_Body. Emit an error on pragma Prag that + -- duplicates previous pragma Prev. + + function Find_Related_Package_Or_Body (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; - -- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global, - -- Refined_Depends, Refined_Global and Refined_Post. Find the declaration - -- of the related subprogram [body or stub] subject to pragma Prag. If flag - -- Do_Checks is set, the routine reports duplicate pragmas and detects - -- improper use of refinement pragmas in stand alone expression functions. - -- The returned value depends on the related pragma as follows: - -- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding - -- N_Subprogram_Declaration node or if the pragma applies to a stand - -- alone body, the N_Subprogram_Body node or Empty if illegal. - -- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield - -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if - -- illegal. + -- Subsidiary to the analysis of pragmas Abstract_State, Initial_Condition, + -- Initializes and Refined_State. Find the declaration of the related + -- package [body] subject to pragma Prag. The return value is either + -- N_Package_Declaration, N_Package_Body or Empty if the placement of + -- the pragma is illegal. If flag Do_Checks is set, the routine reports + -- duplicate pragmas. + function Get_Argument + (Prag : Node_Id; + Spec_Id : Entity_Id := Empty) return Node_Id; + -- Obtain the argument of pragma Prag depending on context and the nature + -- of the pragma. The argument is extracted in the following manner: + -- + -- When the pragma is generated from an aspect, return the corresponding + -- aspect for ASIS or when Spec_Id denotes a generic subprogram. + -- + -- Otherwise return the first argument of Prag + -- + -- Spec_Id denotes the entity of the subprogram spec where Prag resides + function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id; -- If Def_Id refers to a renamed subprogram, then the base subprogram (the -- original one, following the renaming chain) is returned. Otherwise the @@ -254,11 +260,6 @@ -- tagged, unconstrained array, unconstrained record or a record with at -- least one unconstrained component. - procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id); - -- Preanalyze the boolean expressions in the Requires and Ensures arguments - -- of a Test_Case pragma if present (possibly Empty). We treat these as - -- spec expressions (i.e. similar to a default expression). - procedure Record_Possible_Body_Reference (State_Id : Entity_Id; Ref : Node_Id); @@ -276,8 +277,8 @@ procedure Rewrite_Assertion_Kind (N : Node_Id); -- If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class, -- then it is rewritten as an identifier with the corresponding special - -- name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas - -- Check, Check_Policy. + -- name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas Check + -- and Check_Policy. procedure Set_Elab_Unit_Name (N : Node_Id; With_Item : Node_Id); -- Place semantic information on the argument of an Elaborate/Elaborate_All @@ -439,7 +440,7 @@ Subp_Decl := Find_Related_Subprogram_Or_Body (N); Subp_Id := Defining_Entity (Subp_Decl); - All_Cases := Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + All_Cases := Expression (Get_Argument (N, Subp_Id)); -- Single and multiple contract cases must appear in aggregate form. If -- this is not the case, then either the parser of the analysis of the @@ -447,12 +448,8 @@ pragma Assert (Nkind (All_Cases) = N_Aggregate); - if No (Component_Associations (All_Cases)) then - Error_Msg_N ("wrong syntax for constract cases", N); + if Present (Component_Associations (All_Cases)) then - -- Individual contract cases appear as component associations - - else -- Ensure that the formal parameters are visible when analyzing all -- clauses. This falls out of the general rule of aspects pertaining -- to subprogram declarations. Skip the installation for subprogram @@ -461,7 +458,12 @@ if not In_Open_Scopes (Subp_Id) then Restore_Scope := True; Push_Scope (Subp_Id); - Install_Formals (Subp_Id); + + if Is_Generic_Subprogram (Subp_Id) then + Install_Generic_Formals (Subp_Id); + else + Install_Formals (Subp_Id); + end if; end if; CCase := First (Component_Associations (All_Cases)); @@ -473,6 +475,8 @@ if Restore_Scope then End_Scope; end if; + else + Error_Msg_N ("wrong syntax for constract cases", N); end if; end Analyze_Contract_Cases_In_Decl_Part; @@ -872,8 +876,7 @@ SPARK_Msg_NE ("cannot mention state & in global refinement", Item, Item_Id); - SPARK_Msg_N - ("\use its constituents instead", Item); + SPARK_Msg_N ("\use its constituents instead", Item); return; -- If the reference to the abstract state appears in @@ -1557,10 +1560,8 @@ -- Local variables - Deps : constant Node_Id := - Get_Pragma_Arg - (First (Pragma_Argument_Associations (N))); Clause : Node_Id; + Deps : Node_Id; Errors : Nat; Last_Clause : Node_Id; Subp_Decl : Node_Id; @@ -1575,26 +1576,15 @@ Subp_Decl := Find_Related_Subprogram_Or_Body (N); Subp_Id := Defining_Entity (Subp_Decl); + Deps := Expression (Get_Argument (N, Subp_Id)); -- The logic in this routine is used to analyze both pragma Depends and -- pragma Refined_Depends since they have the same syntax and base -- semantics. Find the entity of the corresponding spec when analyzing -- Refined_Depends. - if Nkind (Subp_Decl) = N_Subprogram_Body - and then Present (Corresponding_Spec (Subp_Decl)) - then - Spec_Id := Corresponding_Spec (Subp_Decl); + Spec_Id := Corresponding_Spec_Of (Subp_Decl); - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub - and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) - then - Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); - - else - Spec_Id := Subp_Id; - end if; - -- Empty dependency list if Nkind (Deps) = N_Null then @@ -1648,7 +1638,12 @@ if not In_Open_Scopes (Spec_Id) then Restore_Scope := True; Push_Scope (Spec_Id); - Install_Formals (Spec_Id); + + if Is_Generic_Subprogram (Spec_Id) then + Install_Generic_Formals (Spec_Id); + else + Install_Formals (Spec_Id); + end if; end if; Clause := First (Component_Associations (Deps)); @@ -2189,41 +2184,28 @@ -- Local variables - Items : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Items : Node_Id; Subp_Decl : Node_Id; Restore_Scope : Boolean := False; -- Set True if we do a Push_Scope requiring a Pop_Scope on exit - -- Start of processing for Analyze_Global_In_Decl_List + -- Start of processing for Analyze_Global_In_Decl_Part begin Set_Analyzed (N); - Check_SPARK_Aspect_For_ASIS (N); Subp_Decl := Find_Related_Subprogram_Or_Body (N); Subp_Id := Defining_Entity (Subp_Decl); + Items := Expression (Get_Argument (N, Subp_Id)); -- The logic in this routine is used to analyze both pragma Global and -- pragma Refined_Global since they have the same syntax and base -- semantics. Find the entity of the corresponding spec when analyzing -- Refined_Global. - if Nkind (Subp_Decl) = N_Subprogram_Body - and then Present (Corresponding_Spec (Subp_Decl)) - then - Spec_Id := Corresponding_Spec (Subp_Decl); + Spec_Id := Corresponding_Spec_Of (Subp_Decl); - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub - and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) - then - Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); - - else - Spec_Id := Subp_Id; - end if; - -- There is nothing to be done for a null global list if Nkind (Items) = N_Null then @@ -2241,7 +2223,12 @@ if not In_Open_Scopes (Spec_Id) then Restore_Scope := True; Push_Scope (Spec_Id); - Install_Formals (Spec_Id); + + if Is_Generic_Subprogram (Spec_Id) then + Install_Generic_Formals (Spec_Id); + else + Install_Formals (Spec_Id); + end if; end if; Analyze_Global_List (Items); @@ -2265,8 +2252,7 @@ -------------------------------------------- procedure Analyze_Initial_Condition_In_Decl_Part (N : Node_Id) is - Expr : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Expr : constant Node_Id := Expression (Get_Argument (N)); begin Set_Analyzed (N); @@ -2601,8 +2587,7 @@ -- Local variables - Inits : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Inits : constant Node_Id := Expression (Get_Argument (N)); Init : Node_Id; -- Start of processing for Analyze_Initializes_In_Decl_Part @@ -2610,8 +2595,6 @@ begin Set_Analyzed (N); - Check_SPARK_Aspect_For_ASIS (N); - -- Nothing to do when the initialization list is empty if Nkind (Inits) = N_Null then @@ -2717,6 +2700,9 @@ -- encapsulating state. Indic is the Part_Of indicator. Flag Legal is -- set when the indicator is legal. + procedure Analyze_Pre_Post_Condition; + -- Subsidiary to the analysis of pragmas Precondition and Postcondition + procedure Analyze_Refined_Pragma (Spec_Id : out Entity_Id; Body_Id : out Entity_Id; @@ -2918,54 +2904,12 @@ -- In this version of the procedure, the identifier name is given as -- a string with lower case letters. - procedure Check_Pre_Post; - -- Called to perform checks for Pre, Pre_Class, Post, Post_Class - -- pragmas. These are processed by transformation to equivalent - -- Precondition and Postcondition pragmas, but Pre and Post need an - -- additional check that they are not used in a subprogram body when - -- there is a separate spec present. - - procedure Check_Precondition_Postcondition (In_Body : out Boolean); - -- Called to process a precondition or postcondition pragma. There are - -- three cases: - -- - -- The pragma appears after a subprogram spec - -- - -- If the corresponding check is not enabled, the pragma is analyzed - -- but otherwise ignored and control returns with In_Body set False. - -- - -- If the check is enabled, then the first step is to analyze the - -- pragma, but this is skipped if the subprogram spec appears within - -- a package specification (because this is the case where we delay - -- analysis till the end of the spec). Then (whether or not it was - -- analyzed), the pragma is chained to the subprogram in question - -- (using Pre_Post_Conditions and Next_Pragma) and control returns - -- to the caller with In_Body set False. - -- - -- The pragma appears at the start of subprogram body declarations - -- - -- In this case an immediate return to the caller is made with - -- In_Body set True, and the pragma is NOT analyzed. - -- - -- In all other cases, an error message for bad placement is given - procedure Check_Static_Constraint (Constr : Node_Id); -- Constr is a constraint from an N_Subtype_Indication node from a -- component constraint in an Unchecked_Union type. This routine checks -- that the constraint is static as required by the restrictions for -- Unchecked_Union. - procedure Check_Test_Case; - -- Called to process a test-case pragma. It starts with checking pragma - -- arguments, and the rest of the treatment is similar to the one for - -- pre- and postcondition in Check_Precondition_Postcondition, except - -- the placement rules for the test-case pragma are stricter. These - -- pragmas may only occur after a subprogram spec declared directly - -- in a package spec unit. In this case, the pragma is chained to the - -- subprogram in question (using Contract_Test_Cases and Next_Pragma) - -- and analysis of the pragma is delayed till the end of the spec. In - -- all other cases, an error message for bad placement is given. - procedure Check_Valid_Configuration_Pragma; -- Legality checks for placement of a configuration pragma @@ -2983,11 +2927,21 @@ -- presence of at least one component. UU_Typ is the related Unchecked_ -- Union type. + procedure Create_Generic_Template + (Prag : Node_Id; + Subp_Id : Entity_Id); + -- Subsidiary routine to the processing of pragmas Contract_Cases, + -- Depends, Global, Postcondition, Precondition and Test_Case. Create + -- a generic template for pragma Prag when Prag is a source construct + -- and the related context denoted by Subp_Id is a generic subprogram. + procedure Ensure_Aggregate_Form (Arg : Node_Id); -- Subsidiary routine to the processing of pragmas Abstract_State, -- Contract_Cases, Depends, Global, Initializes, Refined_Depends, - -- Refined_Global and Refined_State. Transform argument Arg into an - -- aggregate if not one already. N_Null is never transformed. + -- Refined_Global and Refined_State. Transform argument Arg into + -- an aggregate if not one already. N_Null is never transformed. + -- Arg may denote an aspect specification or a pragma argument + -- association. procedure Error_Pragma (Msg : String); pragma No_Return (Error_Pragma); @@ -3469,6 +3423,172 @@ Legal := True; end Analyze_Part_Of; + -------------------------------- + -- Analyze_Pre_Post_Condition -- + -------------------------------- + + procedure Analyze_Pre_Post_Condition is + Prag_Iden : constant Node_Id := Pragma_Identifier (N); + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; + + Duplicates_OK : Boolean := False; + -- Flag set when a pre/postcondition allows multiple pragmas of the + -- same kind. + + In_Body_OK : Boolean := False; + -- Flag set when a pre/postcondition is allowed to appear on a body + -- even though the subprogram may have a spec. + + Is_Pre_Post : Boolean := False; + -- Flag set when the pragma is one of Pre, Pre_Class, Post or + -- Post_Class. + + begin + -- Change the name of pragmas Pre, Pre_Class, Post and Post_Class to + -- offer uniformity among the various kinds of pre/postconditions by + -- rewriting the pragma identifier. This allows the retrieval of the + -- original pragma name by routine Original_Aspect_Pragma_Name. + + if Comes_From_Source (N) then + if Nam_In (Pname, Name_Pre, Name_Pre_Class) then + Is_Pre_Post := True; + Set_Class_Present (N, Pname = Name_Pre_Class); + Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Precondition)); + + elsif Nam_In (Pname, Name_Post, Name_Post_Class) then + Is_Pre_Post := True; + Set_Class_Present (N, Pname = Name_Post_Class); + Rewrite (Prag_Iden, Make_Identifier (Loc, Name_Postcondition)); + end if; + end if; + + -- Determine the semantics with respect to duplicates and placement + -- in a body. Pragmas Precondition and Postcondition were introduced + -- before aspects and are not subject to the same aspect-like rules. + + if Nam_In (Pname, Name_Precondition, Name_Postcondition) then + Duplicates_OK := True; + In_Body_OK := True; + end if; + + GNAT_Pragma; + + -- Pragmas Pre, Pre_Class, Post and Post_Class allow for a single + -- argument without an identifier. + + if Is_Pre_Post then + Check_Arg_Count (1); + Check_No_Identifiers; + + -- Pragmas Precondition and Postcondition have complex argument + -- profile. + + else + Check_At_Least_N_Arguments (1); + Check_At_Most_N_Arguments (2); + Check_Optional_Identifier (Arg1, Name_Check); + + if Present (Arg2) then + Check_Optional_Identifier (Arg2, Name_Message); + Preanalyze_Spec_Expression + (Get_Pragma_Arg (Arg2), Standard_String); + end if; + end if; + + -- For a pragma PPC in the extended main source unit, record enabled + -- status in SCO. + -- ??? nothing checks that the pragma is in the main source unit + + if Is_Checked (N) and then not Split_PPC (N) then + Set_SCO_Pragma_Enabled (Loc); + end if; + + -- Ensure the proper placement of the pragma + + Subp_Decl := + Find_Related_Subprogram_Or_Body (N, Do_Checks => not Duplicates_OK); + + -- When a pre/postcondition pragma applies to an abstract subprogram, + -- its original form must be an aspect with 'Class. + + if Nkind (Subp_Decl) = N_Abstract_Subprogram_Declaration then + if not From_Aspect_Specification (N) then + Error_Pragma + ("pragma % cannot be applied to abstract subprogram"); + + elsif not Class_Present (N) then + Error_Pragma + ("aspect % requires ''Class for abstract subprogram"); + end if; + + -- Entry declaration + + elsif Nkind (Subp_Decl) = N_Entry_Declaration then + null; + + -- Generic subprogram declaration + + elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + null; + + -- Subprogram body + + elsif Nkind (Subp_Decl) = N_Subprogram_Body + and then (No (Corresponding_Spec (Subp_Decl)) or In_Body_OK) + then + null; + + -- Subprogram body stub + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then (No (Corresponding_Spec_Of_Stub (Subp_Decl)) or In_Body_OK) + then + null; + + -- Subprogram declaration + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + + -- AI05-0230: When a pre/postcondition pragma applies to a null + -- procedure, its original form must be an aspect with 'Class. + + if Nkind (Specification (Subp_Decl)) = N_Procedure_Specification + and then Null_Present (Specification (Subp_Decl)) + and then From_Aspect_Specification (N) + and then not Class_Present (N) + then + Error_Pragma ("aspect % requires ''Class for null procedure"); + end if; + + -- Otherwise the placement is illegal + + else + Pragma_Misplaced; + return; + end if; + + Subp_Id := Defining_Entity (Subp_Decl); + + -- Construct a generic template for the pragma when the context is a + -- generic subprogram and the pragma is a source construct. + + Create_Generic_Template (N, Subp_Id); + + -- Fully analyze the pragma when it appears inside a subprogram + -- body because it cannot benefit from forward references. + + if Nkind_In (Subp_Decl, N_Subprogram_Body, + N_Subprogram_Body_Stub) + then + Analyze_Pre_Post_Condition_In_Decl_Part (N); + end if; + + -- Chain the pragma on the contract for further processing + + Add_Contract_Item (N, Subp_Id); + end Analyze_Pre_Post_Condition; + ---------------------------- -- Analyze_Refined_Pragma -- ---------------------------- @@ -3492,13 +3612,6 @@ Check_Arg_Count (1); Check_No_Identifiers; - if Nam_In (Pname, Name_Refined_Depends, - Name_Refined_Global, - Name_Refined_State) - then - Ensure_Aggregate_Form (Arg1); - end if; - -- Verify the placement of the pragma and check for duplicates. The -- pragma must apply to a subprogram body [stub]. @@ -3538,7 +3651,7 @@ -- declared in the visible part of a package. Retrieve the context of -- the subprogram declaration. - Spec_Decl := Parent (Parent (Spec_Id)); + Spec_Decl := Unit_Declaration_Node (Spec_Id); if Nkind (Parent (Spec_Decl)) /= N_Package_Specification then Error_Pragma @@ -3549,6 +3662,13 @@ -- If we get here, then the pragma is legal + if Nam_In (Pname, Name_Refined_Depends, + Name_Refined_Global, + Name_Refined_State) + then + Ensure_Aggregate_Form (Get_Argument (N)); + end if; + Legal := True; end Analyze_Refined_Pragma; @@ -4847,363 +4967,6 @@ Check_Optional_Identifier (Arg, Name_Find); end Check_Optional_Identifier; - -------------------- - -- Check_Pre_Post -- - -------------------- - - procedure Check_Pre_Post is - P : Node_Id; - PO : Node_Id; - - begin - if not Is_List_Member (N) then - Pragma_Misplaced; - end if; - - -- If we are within an inlined body, the legality of the pragma - -- has been checked already. - - if In_Inlined_Body then - return; - end if; - - -- Search prior declarations - - P := N; - while Present (Prev (P)) loop - P := Prev (P); - - -- If the previous node is a generic subprogram, do not go to to - -- the original node, which is the unanalyzed tree: we need to - -- attach the pre/postconditions to the analyzed version at this - -- point. They get propagated to the original tree when analyzing - -- the corresponding body. - - if Nkind (P) not in N_Generic_Declaration then - PO := Original_Node (P); - else - PO := P; - end if; - - -- Skip past prior pragma - - if Nkind (PO) = N_Pragma then - null; - - -- Skip stuff not coming from source - - elsif not Comes_From_Source (PO) then - - -- The condition may apply to a subprogram instantiation - - if Nkind (PO) = N_Subprogram_Declaration - and then Present (Generic_Parent (Specification (PO))) - then - return; - - elsif Nkind (PO) = N_Subprogram_Declaration - and then In_Instance - then - return; - - -- For all other cases of non source code, do nothing - - else - null; - end if; - - -- Only remaining possibility is subprogram declaration - - else - return; - end if; - end loop; - - -- If we fall through loop, pragma is at start of list, so see if it - -- is at the start of declarations of a subprogram body. - - PO := Parent (N); - - if Nkind (PO) = N_Subprogram_Body - and then List_Containing (N) = Declarations (PO) - then - -- This is only allowed if there is no separate specification - - if Present (Corresponding_Spec (PO)) then - Error_Pragma - ("pragma% must apply to subprogram specification"); - end if; - - return; - end if; - end Check_Pre_Post; - - -------------------------------------- - -- Check_Precondition_Postcondition -- - -------------------------------------- - - procedure Check_Precondition_Postcondition (In_Body : out Boolean) is - P : Node_Id; - PO : Node_Id; - - procedure Chain_PPC (PO : Node_Id); - -- If PO is an entry or a [generic] subprogram declaration node, then - -- the precondition/postcondition applies to this subprogram and the - -- processing for the pragma is completed. Otherwise the pragma is - -- misplaced. - - --------------- - -- Chain_PPC -- - --------------- - - procedure Chain_PPC (PO : Node_Id) is - S : Entity_Id; - - begin - if Nkind (PO) = N_Abstract_Subprogram_Declaration then - if not From_Aspect_Specification (N) then - Error_Pragma - ("pragma% cannot be applied to abstract subprogram"); - - elsif Class_Present (N) then - null; - - else - Error_Pragma - ("aspect % requires ''Class for abstract subprogram"); - end if; - - -- AI05-0230: The same restriction applies to null procedures. For - -- compatibility with earlier uses of the Ada pragma, apply this - -- rule only to aspect specifications. - - -- The above discrepency needs documentation. Robert is dubious - -- about whether it is a good idea ??? - - elsif Nkind (PO) = N_Subprogram_Declaration - and then Nkind (Specification (PO)) = N_Procedure_Specification - and then Null_Present (Specification (PO)) - and then From_Aspect_Specification (N) - and then not Class_Present (N) - then - Error_Pragma - ("aspect % requires ''Class for null procedure"); - - -- Pre/postconditions are legal on a subprogram body if it is not - -- a completion of a declaration. They are also legal on a stub - -- with no previous declarations (this is checked when processing - -- the corresponding aspects). - - elsif Nkind (PO) = N_Subprogram_Body - and then Acts_As_Spec (PO) - then - null; - - elsif Nkind (PO) = N_Subprogram_Body_Stub then - null; - - elsif not Nkind_In (PO, N_Subprogram_Declaration, - N_Expression_Function, - N_Generic_Subprogram_Declaration, - N_Entry_Declaration) - then - Pragma_Misplaced; - end if; - - -- Here if we have [generic] subprogram or entry declaration - - if Nkind (PO) = N_Entry_Declaration then - S := Defining_Entity (PO); - else - S := Defining_Unit_Name (Specification (PO)); - - if Nkind (S) = N_Defining_Program_Unit_Name then - S := Defining_Identifier (S); - end if; - end if; - - -- Note: we do not analyze the pragma at this point. Instead we - -- delay this analysis until the end of the declarative part in - -- which the pragma appears. This implements the required delay - -- in this analysis, allowing forward references. The analysis - -- happens at the end of Analyze_Declarations. - - -- Chain spec PPC pragma to list for subprogram - - Add_Contract_Item (N, S); - - -- Return indicating spec case - - In_Body := False; - return; - end Chain_PPC; - - -- Start of processing for Check_Precondition_Postcondition - - begin - if not Is_List_Member (N) then - Pragma_Misplaced; - end if; - - -- Preanalyze message argument if present. Visibility in this - -- argument is established at the point of pragma occurrence. - - if Arg_Count = 2 then - Check_Optional_Identifier (Arg2, Name_Message); - Preanalyze_Spec_Expression - (Get_Pragma_Arg (Arg2), Standard_String); - end if; - - -- For a pragma PPC in the extended main source unit, record enabled - -- status in SCO. - - if Is_Checked (N) and then not Split_PPC (N) then - Set_SCO_Pragma_Enabled (Loc); - end if; - - -- If we are within an inlined body, the legality of the pragma - -- has been checked already. - - if In_Inlined_Body then - In_Body := True; - return; - end if; - - -- Search prior declarations - - P := N; - while Present (Prev (P)) loop - P := Prev (P); - - -- If the previous node is a generic subprogram, do not go to to - -- the original node, which is the unanalyzed tree: we need to - -- attach the pre/postconditions to the analyzed version at this - -- point. They get propagated to the original tree when analyzing - -- the corresponding body. - - if Nkind (P) not in N_Generic_Declaration then - PO := Original_Node (P); - else - PO := P; - end if; - - -- Skip past prior pragma - - if Nkind (PO) = N_Pragma then - null; - - -- Skip stuff not coming from source - - elsif not Comes_From_Source (PO) then - - -- The condition may apply to a subprogram instantiation - - if Nkind (PO) = N_Subprogram_Declaration - and then Present (Generic_Parent (Specification (PO))) - then - Chain_PPC (PO); - return; - - elsif Nkind (PO) = N_Subprogram_Declaration - and then In_Instance - then - Chain_PPC (PO); - return; - - -- For all other cases of non source code, do nothing - - else - null; - end if; - - -- Only remaining possibility is subprogram declaration - - else - Chain_PPC (PO); - return; - end if; - end loop; - - -- If we fall through loop, pragma is at start of list, so see if it - -- is at the start of declarations of a subprogram body. - - PO := Parent (N); - - if Nkind (PO) = N_Subprogram_Body - and then List_Containing (N) = Declarations (PO) - then - if Operating_Mode /= Generate_Code or else Inside_A_Generic then - - -- Analyze pragma expression for correctness and for ASIS use - - Preanalyze_Assert_Expression - (Get_Pragma_Arg (Arg1), Standard_Boolean); - - -- In ASIS mode, for a pragma generated from a source aspect, - -- also analyze the original aspect expression. - - if ASIS_Mode and then Present (Corresponding_Aspect (N)) then - Preanalyze_Assert_Expression - (Expression (Corresponding_Aspect (N)), Standard_Boolean); - end if; - end if; - - -- Retain copy of the pre/postcondition pragma in GNATprove mode. - -- The copy is needed because the pragma is expanded into other - -- constructs which are not acceptable in the N_Contract node. - - if Acts_As_Spec (PO) and then GNATprove_Mode then - declare - Prag : constant Node_Id := New_Copy_Tree (N); - - begin - -- Preanalyze the pragma - - Preanalyze_Assert_Expression - (Get_Pragma_Arg - (First (Pragma_Argument_Associations (Prag))), - Standard_Boolean); - - -- Preanalyze the corresponding aspect (if any) - - if Present (Corresponding_Aspect (Prag)) then - Preanalyze_Assert_Expression - (Expression (Corresponding_Aspect (Prag)), - Standard_Boolean); - end if; - - -- Chain the copy on the contract of the body - - Add_Contract_Item - (Prag, Defining_Unit_Name (Specification (PO))); - end; - end if; - - In_Body := True; - return; - - -- See if it is in the pragmas after a library level subprogram - - elsif Nkind (PO) = N_Compilation_Unit_Aux then - - -- In GNATprove mode, analyze pragma expression for correctness, - -- as it is not expanded later. Ditto in ASIS_Mode where there is - -- no later point at which the aspect will be analyzed. - - if GNATprove_Mode or ASIS_Mode then - Analyze_Pre_Post_Condition_In_Decl_Part - (N, Defining_Entity (Unit (Parent (PO)))); - end if; - - Chain_PPC (Unit (Parent (PO))); - return; - end if; - - -- If we fall through, pragma was misplaced - - Pragma_Misplaced; - end Check_Precondition_Postcondition; - ----------------------------- -- Check_Static_Constraint -- ----------------------------- @@ -5265,178 +5028,6 @@ end case; end Check_Static_Constraint; - --------------------- - -- Check_Test_Case -- - --------------------- - - procedure Check_Test_Case is - P : Node_Id; - PO : Node_Id; - - procedure Chain_CTC (PO : Node_Id); - -- If PO is a [generic] subprogram declaration node, then the - -- test-case applies to this subprogram and the processing for - -- the pragma is completed. Otherwise the pragma is misplaced. - - --------------- - -- Chain_CTC -- - --------------- - - procedure Chain_CTC (PO : Node_Id) is - Name : constant String_Id := Get_Name_From_CTC_Pragma (N); - CTC : Node_Id; - S : Entity_Id; - - begin - if Nkind (PO) = N_Abstract_Subprogram_Declaration then - Error_Pragma - ("pragma% cannot be applied to abstract subprogram"); - - elsif Nkind (PO) = N_Entry_Declaration then - Error_Pragma ("pragma% cannot be applied to entry"); - - elsif not Nkind_In (PO, N_Subprogram_Declaration, - N_Generic_Subprogram_Declaration) - then - Pragma_Misplaced; - end if; - - -- Here if we have [generic] subprogram declaration - - S := Defining_Unit_Name (Specification (PO)); - - -- Note: we do not analyze the pragma at this point. Instead we - -- delay this analysis until the end of the declarative part in - -- which the pragma appears. This implements the required delay - -- in this analysis, allowing forward references. The analysis - -- happens at the end of Analyze_Declarations. - - -- There should not be another test-case with the same name - -- associated to this subprogram. - - CTC := Contract_Test_Cases (Contract (S)); - while Present (CTC) loop - - -- Omit pragma Contract_Cases because it does not introduce - -- a unique case name and it does not follow the syntax of - -- Test_Case. - - if Pragma_Name (CTC) = Name_Contract_Cases then - null; - - elsif String_Equal (Name, Get_Name_From_CTC_Pragma (CTC)) then - Error_Msg_Sloc := Sloc (CTC); - Error_Pragma ("name for pragma% is already used#"); - end if; - - CTC := Next_Pragma (CTC); - end loop; - - -- Chain spec CTC pragma to list for subprogram - - Add_Contract_Item (N, S); - end Chain_CTC; - - -- Start of processing for Check_Test_Case - - begin - -- First check pragma arguments - - Check_At_Least_N_Arguments (2); - Check_At_Most_N_Arguments (4); - Check_Arg_Order - ((Name_Name, Name_Mode, Name_Requires, Name_Ensures)); - - Check_Optional_Identifier (Arg1, Name_Name); - Check_Arg_Is_OK_Static_Expression (Arg1, Standard_String); - - -- In ASIS mode, for a pragma generated from a source aspect, also - -- analyze the original aspect expression. - - if ASIS_Mode and then Present (Corresponding_Aspect (N)) then - Check_Expr_Is_OK_Static_Expression - (Original_Node (Get_Pragma_Arg (Arg1)), Standard_String); - end if; - - Check_Optional_Identifier (Arg2, Name_Mode); - Check_Arg_Is_One_Of (Arg2, Name_Nominal, Name_Robustness); - - if Arg_Count = 4 then - Check_Identifier (Arg3, Name_Requires); - Check_Identifier (Arg4, Name_Ensures); - - elsif Arg_Count = 3 then - Check_Identifier_Is_One_Of (Arg3, Name_Requires, Name_Ensures); - end if; - - -- Check pragma placement - - if not Is_List_Member (N) then - Pragma_Misplaced; - end if; - - -- Test-case should only appear in package spec unit - - if Get_Source_Unit (N) = No_Unit - or else not Nkind_In (Sinfo.Unit (Cunit (Current_Sem_Unit)), - N_Package_Declaration, - N_Generic_Package_Declaration) - then - Pragma_Misplaced; - end if; - - -- Search prior declarations - - P := N; - while Present (Prev (P)) loop - P := Prev (P); - - -- If the previous node is a generic subprogram, do not go to to - -- the original node, which is the unanalyzed tree: we need to - -- attach the test-case to the analyzed version at this point. - -- They get propagated to the original tree when analyzing the - -- corresponding body. - - if Nkind (P) not in N_Generic_Declaration then - PO := Original_Node (P); - else - PO := P; - end if; - - -- Skip past prior pragma - - if Nkind (PO) = N_Pragma then - null; - - -- Skip stuff not coming from source - - elsif not Comes_From_Source (PO) then - null; - - -- Only remaining possibility is subprogram declaration. First - -- check that it is declared directly in a package declaration. - -- This may be either the package declaration for the current unit - -- being defined or a local package declaration. - - elsif not Present (Parent (Parent (PO))) - or else not Present (Parent (Parent (Parent (PO)))) - or else not Nkind_In (Parent (Parent (PO)), - N_Package_Declaration, - N_Generic_Package_Declaration) - then - Pragma_Misplaced; - - else - Chain_CTC (PO); - return; - end if; - end loop; - - -- If we fall through, pragma was misplaced - - Pragma_Misplaced; - end Check_Test_Case; - -------------------------------------- -- Check_Valid_Configuration_Pragma -- -------------------------------------- @@ -5609,23 +5200,47 @@ end loop; end Check_Variant; + ----------------------------- + -- Create_Generic_Template -- + ----------------------------- + + procedure Create_Generic_Template + (Prag : Node_Id; + Subp_Id : Entity_Id) + is + begin + if Comes_From_Source (Prag) + and then Is_Generic_Subprogram (Subp_Id) + then + Rewrite + (Prag, Copy_Generic_Node (Prag, Empty, Instantiating => False)); + end if; + end Create_Generic_Template; + --------------------------- -- Ensure_Aggregate_Form -- --------------------------- procedure Ensure_Aggregate_Form (Arg : Node_Id) is - Expr : constant Node_Id := Get_Pragma_Arg (Arg); - Loc : constant Source_Ptr := Sloc (Arg); - Nam : constant Name_Id := Chars (Arg); + Expr : constant Node_Id := Expression (Arg); + Loc : constant Source_Ptr := Sloc (Expr); Comps : List_Id := No_List; Exprs : List_Id := No_List; + Nam : Name_Id; CFSD : constant Boolean := Get_Comes_From_Source_Default; -- Used to restore Comes_From_Source_Default begin + if Nkind (Arg) = N_Aspect_Specification then + Nam := No_Name; + else + pragma Assert (Nkind (Arg) = N_Pragma_Argument_Association); + Nam := Chars (Arg); + end if; + -- The argument is already in aggregate form, but the presence of a - -- name causes this to be interpreted as a named association which in + -- name causes this to be interpreted as named association which in -- turn must be converted into an aggregate. -- pragma Global (In_Out => (A, B, C)) @@ -5671,7 +5286,9 @@ -- Remove the pragma argument name as this information has been -- captured in the aggregate. - Set_Chars (Arg, No_Name); + if Nkind (Arg) = N_Pragma_Argument_Association then + Set_Chars (Arg, No_Name); + end if; Set_Expression (Arg, Make_Aggregate (Loc, @@ -5917,7 +5534,7 @@ -- Get name from corresponding aspect - Error_Msg_Name_1 := Original_Aspect_Name (N); + Error_Msg_Name_1 := Original_Aspect_Pragma_Name (N); end if; -- Return possibly modified message @@ -9731,7 +9348,7 @@ -- Here to start processing for recognized pragma Prag_Id := Get_Pragma_Id (Pname); - Pname := Original_Aspect_Name (N); + Pname := Original_Aspect_Pragma_Name (N); -- Capture setting of Opt.Uneval_Old @@ -10463,9 +10080,9 @@ -- Local variables - Context : constant Node_Id := Parent (Parent (N)); - Pack_Id : Entity_Id; - State : Node_Id; + Pack_Decl : Node_Id; + Pack_Id : Entity_Id; + State : Node_Id; -- Start of processing for Abstract_State @@ -10473,20 +10090,26 @@ GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); - Ensure_Aggregate_Form (Arg1); + Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True); + -- Ensure the proper placement of the pragma. Abstract states must -- be associated with a package declaration. - if not Nkind_In (Context, N_Generic_Package_Declaration, - N_Package_Declaration) + if Nkind_In (Pack_Decl, N_Generic_Package_Declaration, + N_Package_Declaration) then + null; + + -- Otherwise the pragma is associated with an illegal construct + + else Pragma_Misplaced; return; end if; - State := Expression (Arg1); - Pack_Id := Defining_Entity (Context); + Ensure_Aggregate_Form (Get_Argument (N)); + Pack_Id := Defining_Entity (Pack_Decl); -- Mark the associated package as Ghost if it is subject to aspect -- or pragma Ghost as this affects the declaration of an abstract @@ -10496,6 +10119,8 @@ Set_Is_Ghost_Entity (Pack_Id); end if; + State := Expression (Get_Argument (N)); + -- Multiple non-null abstract states appear as an aggregate if Nkind (State) = N_Aggregate then @@ -12284,12 +11909,12 @@ when Pragma_Contract_Cases => Contract_Cases : declare Subp_Decl : Node_Id; + Subp_Id : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); - Ensure_Aggregate_Form (Arg1); -- The pragma is analyzed at the end of the declarative part which -- contains the related subprogram. Reset the analyzed flag. @@ -12303,7 +11928,9 @@ Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True); - if Nkind (Subp_Decl) = N_Subprogram_Declaration then + -- Generic subprogram + + if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then null; -- Body acts as spec @@ -12320,30 +11947,35 @@ then null; + -- Subprogram + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + null; + else Pragma_Misplaced; return; end if; - -- When the pragma appears on a subprogram body, perform the full - -- analysis now. + Subp_Id := Defining_Entity (Subp_Decl); - if Nkind (Subp_Decl) = N_Subprogram_Body then - Analyze_Contract_Cases_In_Decl_Part (N); + Ensure_Aggregate_Form (Get_Argument (N, Subp_Id)); - -- When Contract_Cases applies to a subprogram compilation unit, - -- the corresponding pragma is placed after the unit's declaration - -- node and needs to be analyzed immediately. + -- Construct a generic template for the pragma when the context is + -- a generic subprogram and the pragma is a source construct. - elsif Nkind (Subp_Decl) = N_Subprogram_Declaration - and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit - then + Create_Generic_Template (N, Subp_Id); + + -- Fully analyze the pragma when it appears inside a subprogram + -- body because it cannot benefit from forward references. + + if Nkind (Subp_Decl) = N_Subprogram_Body then Analyze_Contract_Cases_In_Decl_Part (N); end if; -- Chain the pragma on the contract for further processing - Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + Add_Contract_Item (N, Subp_Id); end Contract_Cases; ---------------- @@ -12990,11 +12622,11 @@ when Pragma_Depends => Depends : declare Subp_Decl : Node_Id; + Subp_Id : Entity_Id; begin GNAT_Pragma; Check_Arg_Count (1); - Ensure_Aggregate_Form (Arg1); -- Ensure the proper placement of the pragma. Depends must be -- associated with a subprogram declaration or a body that acts @@ -13003,12 +12635,9 @@ Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True); - if Nkind (Subp_Decl) = N_Subprogram_Declaration then - null; - -- Body acts as spec - elsif Nkind (Subp_Decl) = N_Subprogram_Body + if Nkind (Subp_Decl) = N_Subprogram_Body and then No (Corresponding_Spec (Subp_Decl)) then null; @@ -13020,30 +12649,35 @@ then null; + -- Subprogram declaration + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + null; + else Pragma_Misplaced; return; end if; + Subp_Id := Defining_Entity (Subp_Decl); + + Ensure_Aggregate_Form (Get_Argument (N, Subp_Id)); + + -- Construct a generic template for the pragma when the context is + -- a generic subprogram and the pragma is a source construct. + + Create_Generic_Template (N, Subp_Id); + -- When the pragma appears on a subprogram body, perform the full -- analysis now. if Nkind (Subp_Decl) = N_Subprogram_Body then Analyze_Depends_In_Decl_Part (N); - - -- When Depends applies to a subprogram compilation unit, the - -- corresponding pragma is placed after the unit's declaration - -- node and needs to be analyzed immediately. - - elsif Nkind (Subp_Decl) = N_Subprogram_Declaration - and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit - then - Analyze_Depends_In_Decl_Part (N); end if; -- Chain the pragma on the contract for further processing - Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + Add_Contract_Item (N, Subp_Id); end Depends; --------------------- @@ -13276,13 +12910,13 @@ -- gnatwl/-gnatwE (elaboration warnings enabled) switches set. if Elab_Warnings - and not Dynamic_Elaboration_Checks + and not Dynamic_Elaboration_Checks - -- pragma Elaborate not allowed in SPARK mode anyway. We - -- already complained about it, no point in generating any - -- further complaint. + -- pragma Elaborate not allowed in SPARK mode anyway. We + -- already complained about it, no point in generating any + -- further complaint. - and SPARK_Mode /= On + and SPARK_Mode /= On then Error_Msg_N ("?l?use of pragma Elaborate may not be safe", N); @@ -13910,89 +13544,58 @@ -- pragma Extensions_Visible [ (boolean_EXPRESSION) ]; when Pragma_Extensions_Visible => Extensions_Visible : declare - Context : constant Node_Id := Parent (N); - Expr : Node_Id; - Formal : Entity_Id; - Orig_Stmt : Node_Id; - Subp : Entity_Id; - Stmt : Node_Id; - + Expr : Node_Id; + Formal : Entity_Id; Has_OK_Formal : Boolean := False; + Spec_Id : Entity_Id; + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; Check_At_Most_N_Arguments (1); - Subp := Empty; - Stmt := Prev (N); - while Present (Stmt) loop + Subp_Decl := + Find_Related_Subprogram_Or_Body (N, Do_Checks => True); - -- Skip prior pragmas, but check for duplicates + -- Generic subprogram declaration - if Nkind (Stmt) = N_Pragma then - if Pragma_Name (Stmt) = Pname then - Error_Msg_Name_1 := Pname; - Error_Msg_Sloc := Sloc (Stmt); - Error_Msg_N ("pragma % duplicates pragma declared#", N); - end if; + if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + null; - -- Skip internally generated code + -- Body acts as spec - elsif not Comes_From_Source (Stmt) then - Orig_Stmt := Original_Node (Stmt); + elsif Nkind (Subp_Decl) = N_Subprogram_Body + and then No (Corresponding_Spec (Subp_Decl)) + then + null; - -- When pragma Ghost applies to an expression function, the - -- expression function is transformed into a subprogram. + -- Body stub acts as spec - if Nkind (Stmt) = N_Subprogram_Declaration - and then Comes_From_Source (Orig_Stmt) - and then Nkind (Orig_Stmt) = N_Expression_Function - then - Subp := Defining_Entity (Stmt); - exit; - end if; + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + null; - -- The associated [generic] subprogram declaration has been - -- found, stop the search. + -- Subprogram declaration - elsif Nkind_In (Stmt, N_Generic_Subprogram_Declaration, - N_Subprogram_Declaration) - then - Subp := Defining_Entity (Stmt); - exit; + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + null; - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. + -- Otherwise the pragma is associated with an illegal construct - else - Error_Pragma ("pragma % must apply to a subprogram"); - return; - end if; - - Stmt := Prev (Stmt); - end loop; - - -- When the pragma applies to a stand alone subprogram body, it - -- appears within the declarations of the body. In that case the - -- enclosing construct is the proper context. This check is done - -- after the traversal above to allow for duplicate detection. - - if No (Subp) - and then Nkind (Context) = N_Subprogram_Body - and then No (Corresponding_Spec (Context)) - then - Subp := Defining_Entity (Context); - end if; - - if No (Subp) then + else Error_Pragma ("pragma % must apply to a subprogram"); return; end if; + Spec_Id := Corresponding_Spec_Of (Subp_Decl); + Subp_Id := Defining_Entity (Subp_Decl); + -- Examine the formals of the related subprogram - Formal := First_Formal (Subp); + Formal := First_Formal (Spec_Id); while Present (Formal) loop -- At least one of the formals is of a specific tagged type, @@ -14022,14 +13625,19 @@ Error_Msg_N (Fix_Error ("incorrect placement of pragma %"), N); Error_Msg_NE ("\subprogram & lacks parameter of specific tagged or " - & "generic private type", N, Subp); + & "generic private type", N, Spec_Id); return; end if; + -- Construct a generic template for the pragma when the context is + -- a generic subprogram and the pragma is a source construct. + + Create_Generic_Template (N, Subp_Id); + -- Analyze the Boolean expression (if any) if Present (Arg1) then - Expr := Get_Pragma_Arg (Arg1); + Expr := Expression (Get_Argument (N)); Analyze_And_Resolve (Expr, Standard_Boolean); @@ -14042,7 +13650,7 @@ -- Chain the pragma on the contract for further processing - Add_Contract_Item (N, Subp); + Add_Contract_Item (N, Subp_Id); end Extensions_Visible; -------------- @@ -14444,11 +14052,11 @@ when Pragma_Global => Global : declare Subp_Decl : Node_Id; + Subp_Id : Entity_Id; begin GNAT_Pragma; Check_Arg_Count (1); - Ensure_Aggregate_Form (Arg1); -- Ensure the proper placement of the pragma. Global must be -- associated with a subprogram declaration or a body that acts @@ -14457,12 +14065,9 @@ Subp_Decl := Find_Related_Subprogram_Or_Body (N, Do_Checks => True); - if Nkind (Subp_Decl) = N_Subprogram_Declaration then - null; - -- Body acts as spec - elsif Nkind (Subp_Decl) = N_Subprogram_Body + if Nkind (Subp_Decl) = N_Subprogram_Body and then No (Corresponding_Spec (Subp_Decl)) then null; @@ -14474,30 +14079,35 @@ then null; + -- Subprogram declaration + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + null; + else Pragma_Misplaced; return; end if; + Subp_Id := Defining_Entity (Subp_Decl); + + Ensure_Aggregate_Form (Get_Argument (N, Subp_Id)); + + -- Construct a generic template for the pragma when the context is + -- a generic subprogram and the pragma is a source construct. + + Create_Generic_Template (N, Subp_Id); + -- When the pragma appears on a subprogram body, perform the full -- analysis now. if Nkind (Subp_Decl) = N_Subprogram_Body then Analyze_Global_In_Decl_Part (N); - - -- When Global applies to a subprogram compilation unit, the - -- corresponding pragma is placed after the unit's declaration - -- node and needs to be analyzed immediately. - - elsif Nkind (Subp_Decl) = N_Subprogram_Declaration - and then Nkind (Parent (Subp_Decl)) = N_Compilation_Unit - then - Analyze_Global_In_Decl_Part (N); end if; -- Chain the pragma on the contract for further processing - Add_Contract_Item (N, Defining_Entity (Subp_Decl)); + Add_Contract_Item (N, Subp_Id); end Global; ----------- @@ -15046,59 +14656,37 @@ -- pragma Initial_Condition (boolean_EXPRESSION); when Pragma_Initial_Condition => Initial_Condition : declare - Context : constant Node_Id := Parent (Parent (N)); - Pack_Id : Entity_Id; - Stmt : Node_Id; + Pack_Decl : Node_Id; + Pack_Id : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); + Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True); + -- Ensure the proper placement of the pragma. Initial_Condition -- must be associated with a package declaration. - if not Nkind_In (Context, N_Generic_Package_Declaration, - N_Package_Declaration) + if Nkind_In (Pack_Decl, N_Generic_Package_Declaration, + N_Package_Declaration) then + null; + + -- Otherwise the pragma is associated with an illegal context + + else Pragma_Misplaced; return; end if; - Stmt := Prev (N); - while Present (Stmt) loop - - -- Skip prior pragmas, but check for duplicates - - if Nkind (Stmt) = N_Pragma then - if Pragma_Name (Stmt) = Pname then - Error_Msg_Name_1 := Pname; - Error_Msg_Sloc := Sloc (Stmt); - Error_Msg_N ("pragma % duplicates pragma declared #", N); - end if; - - -- Skip internally generated code - - elsif not Comes_From_Source (Stmt) then - null; - - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. - - else - Pragma_Misplaced; - return; - end if; - - Stmt := Prev (Stmt); - end loop; - -- The pragma must be analyzed at the end of the visible -- declarations of the related package. Save the pragma for later -- (see Analyze_Initial_Condition_In_Decl_Part) by adding it to -- the contract of the package. - Pack_Id := Defining_Entity (Context); + Pack_Id := Defining_Entity (Pack_Decl); Add_Contract_Item (N, Pack_Id); -- Verify the declaration order of pragma Initial_Condition with @@ -15161,60 +14749,39 @@ -- INPUT ::= name when Pragma_Initializes => Initializes : declare - Context : constant Node_Id := Parent (Parent (N)); - Pack_Id : Entity_Id; - Stmt : Node_Id; + Pack_Decl : Node_Id; + Pack_Id : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); - Ensure_Aggregate_Form (Arg1); + Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True); + -- Ensure the proper placement of the pragma. Initializes must be -- associated with a package declaration. - if not Nkind_In (Context, N_Generic_Package_Declaration, - N_Package_Declaration) + if Nkind_In (Pack_Decl, N_Generic_Package_Declaration, + N_Package_Declaration) then + null; + + -- Otherwise the pragma is associated with an illegal construc + + else Pragma_Misplaced; return; end if; - Stmt := Prev (N); - while Present (Stmt) loop + Ensure_Aggregate_Form (Get_Argument (N)); - -- Skip prior pragmas, but check for duplicates - - if Nkind (Stmt) = N_Pragma then - if Pragma_Name (Stmt) = Pname then - Error_Msg_Name_1 := Pname; - Error_Msg_Sloc := Sloc (Stmt); - Error_Msg_N ("pragma % duplicates pragma declared #", N); - end if; - - -- Skip internally generated code - - elsif not Comes_From_Source (Stmt) then - null; - - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. - - else - Pragma_Misplaced; - return; - end if; - - Stmt := Prev (Stmt); - end loop; - -- The pragma must be analyzed at the end of the visible -- declarations of the related package. Save the pragma for later -- (see Analyze_Initializes_In_Decl_Part) by adding it to the -- contract of the package. - Pack_Id := Defining_Entity (Context); + Pack_Id := Defining_Entity (Pack_Decl); Add_Contract_Item (N, Pack_Id); -- Verify the declaration order of pragmas Abstract_State and @@ -17992,153 +17559,34 @@ Check_Arg_Is_One_Of (Arg1, Name_On, Name_Off); Polling_Required := (Chars (Get_Pragma_Arg (Arg1)) = Name_On); - ------------------ - -- Post[_Class] -- - ------------------ + ----------------------------------- + -- Post/Post_Class/Postcondition -- + ----------------------------------- -- pragma Post (Boolean_EXPRESSION); -- pragma Post_Class (Boolean_EXPRESSION); - - when Pragma_Post | Pragma_Post_Class => Post : declare - PC_Pragma : Node_Id; - - begin - GNAT_Pragma; - Check_Arg_Count (1); - Check_No_Identifiers; - Check_Pre_Post; - - -- Rewrite Post[_Class] pragma as Postcondition pragma setting the - -- flag Class_Present to True for the Post_Class case. - - Set_Class_Present (N, Prag_Id = Pragma_Post_Class); - PC_Pragma := New_Copy (N); - Set_Pragma_Identifier - (PC_Pragma, Make_Identifier (Loc, Name_Postcondition)); - Rewrite (N, PC_Pragma); - Set_Analyzed (N, False); - Analyze (N); - end Post; - - ------------------- - -- Postcondition -- - ------------------- - -- pragma Postcondition ([Check =>] Boolean_EXPRESSION -- [,[Message =>] String_EXPRESSION]); - when Pragma_Postcondition => Postcondition : declare - In_Body : Boolean; + when Pragma_Post | + Pragma_Post_Class | + Pragma_Postcondition => + Analyze_Pre_Post_Condition; - begin - GNAT_Pragma; - Check_At_Least_N_Arguments (1); - Check_At_Most_N_Arguments (2); - Check_Optional_Identifier (Arg1, Name_Check); + -------------------------------- + -- Pre/Pre_Class/Precondition -- + -------------------------------- - -- Verify the proper placement of the pragma. The remainder of the - -- processing is found in Sem_Ch6/Sem_Ch7. - - Check_Precondition_Postcondition (In_Body); - - -- When the pragma is a source construct appearing inside a body, - -- preanalyze the boolean_expression to detect illegal forward - -- references: - - -- procedure P is - -- pragma Postcondition (X'Old ...); - -- X : ... - - if Comes_From_Source (N) and then In_Body then - Preanalyze_Spec_Expression (Expression (Arg1), Any_Boolean); - end if; - end Postcondition; - - ----------------- - -- Pre[_Class] -- - ----------------- - -- pragma Pre (Boolean_EXPRESSION); -- pragma Pre_Class (Boolean_EXPRESSION); - - when Pragma_Pre | Pragma_Pre_Class => Pre : declare - PC_Pragma : Node_Id; - - begin - GNAT_Pragma; - Check_Arg_Count (1); - Check_No_Identifiers; - Check_Pre_Post; - - -- Rewrite Pre[_Class] pragma as Precondition pragma setting the - -- flag Class_Present to True for the Pre_Class case. - - Set_Class_Present (N, Prag_Id = Pragma_Pre_Class); - PC_Pragma := New_Copy (N); - Set_Pragma_Identifier - (PC_Pragma, Make_Identifier (Loc, Name_Precondition)); - Rewrite (N, PC_Pragma); - Set_Analyzed (N, False); - Analyze (N); - end Pre; - - ------------------ - -- Precondition -- - ------------------ - -- pragma Precondition ([Check =>] Boolean_EXPRESSION -- [,[Message =>] String_EXPRESSION]); - when Pragma_Precondition => Precondition : declare - In_Body : Boolean; + when Pragma_Pre | + Pragma_Pre_Class | + Pragma_Precondition => + Analyze_Pre_Post_Condition; - begin - GNAT_Pragma; - Check_At_Least_N_Arguments (1); - Check_At_Most_N_Arguments (2); - Check_Optional_Identifier (Arg1, Name_Check); - Check_Precondition_Postcondition (In_Body); - - -- If in spec, nothing more to do. If in body, then we convert - -- the pragma to an equivalent pragma Check. That works fine since - -- pragma Check will analyze the condition in the proper context. - - -- The form of the pragma Check is either: - - -- pragma Check (Precondition, cond [, msg]) - -- or - -- pragma Check (Pre, cond [, msg]) - - -- We use the Pre form if this pragma derived from a Pre aspect. - -- This is needed to make sure that the right set of Policy - -- pragmas are checked. - - if In_Body then - - -- Rewrite as Check pragma - - Rewrite (N, - Make_Pragma (Loc, - Chars => Name_Check, - Pragma_Argument_Associations => New_List ( - Make_Pragma_Argument_Association (Loc, - Expression => Make_Identifier (Loc, Pname)), - - Make_Pragma_Argument_Association (Sloc (Arg1), - Expression => - Relocate_Node (Get_Pragma_Arg (Arg1)))))); - - if Arg_Count = 2 then - Append_To (Pragma_Argument_Associations (N), - Make_Pragma_Argument_Association (Sloc (Arg2), - Expression => - Relocate_Node (Get_Pragma_Arg (Arg2)))); - end if; - - Analyze (N); - end if; - end Precondition; - --------------- -- Predicate -- --------------- @@ -19000,33 +18448,19 @@ -- pragma Refined_Post (boolean_EXPRESSION); when Pragma_Refined_Post => Refined_Post : declare - Body_Id : Entity_Id; - Legal : Boolean; - Result_Seen : Boolean := False; - Spec_Id : Entity_Id; + Body_Id : Entity_Id; + Legal : Boolean; + Spec_Id : Entity_Id; begin Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal); - -- Analyze the boolean expression as a "spec expression" + -- Fully analyze the pragma when it appears inside a subprogram + -- body because it cannot benefit from forward references. if Legal then - Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id); + Analyze_Pre_Post_Condition_In_Decl_Part (N); - -- Verify that the refined postcondition mentions attribute - -- 'Result and its expression introduces a post-state. - - if Warn_On_Suspicious_Contract - and then Ekind_In (Spec_Id, E_Function, E_Generic_Function) - then - Check_Result_And_Post_State (N, Result_Seen); - - if not Result_Seen then - Error_Pragma - ("pragma % does not mention function result?T?"); - end if; - end if; - -- Chain the pragma on the contract for easy retrieval Add_Contract_Item (N, Body_Id); @@ -19053,53 +18487,31 @@ -- CONSTITUENT ::= object_NAME | state_NAME when Pragma_Refined_State => Refined_State : declare - Context : constant Node_Id := Parent (N); - Spec_Id : Entity_Id; - Stmt : Node_Id; + Pack_Decl : Node_Id; + Spec_Id : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; Check_Arg_Count (1); + Pack_Decl := Find_Related_Package_Or_Body (N, Do_Checks => True); + -- Ensure the proper placement of the pragma. Refined states must -- be associated with a package body. - if Nkind (Context) /= N_Package_Body then + if Nkind (Pack_Decl) = N_Package_Body then + null; + + -- Otherwise the pragma is associated with an illegal construct + + else Pragma_Misplaced; return; end if; - Stmt := Prev (N); - while Present (Stmt) loop + Spec_Id := Corresponding_Spec (Pack_Decl); - -- Skip prior pragmas, but check for duplicates - - if Nkind (Stmt) = N_Pragma then - if Pragma_Name (Stmt) = Pname then - Error_Msg_Name_1 := Pname; - Error_Msg_Sloc := Sloc (Stmt); - Error_Msg_N ("pragma % duplicates pragma declared #", N); - end if; - - -- Skip internally generated code - - elsif not Comes_From_Source (Stmt) then - null; - - -- The pragma does not apply to a legal construct, issue an - -- error and stop the analysis. - - else - Pragma_Misplaced; - return; - end if; - - Stmt := Prev (Stmt); - end loop; - - Spec_Id := Corresponding_Spec (Context); - -- State refinement is allowed only when the corresponding package -- declaration has non-null pragma Abstract_State. Refinement not -- enforced when SPARK checks are suppressed (SPARK RM 7.2.2(3)). @@ -19117,10 +18529,10 @@ -- The pragma must be analyzed at the end of the declarations as -- it has visibility over the whole declarative region. Save the - -- pragma for later (see Analyze_Refined_Depends_In_Decl_Part) by + -- pragma for later (see Analyze_Refined_State_In_Decl_Part) by -- adding it to the contract of the package body. - Add_Contract_Item (N, Defining_Entity (Context)); + Add_Contract_Item (N, Defining_Entity (Pack_Decl)); end Refined_State; ----------------------- @@ -20661,10 +20073,178 @@ -- MODE_TYPE ::= Nominal | Robustness - when Pragma_Test_Case => + when Pragma_Test_Case => Test_Case : declare + procedure Check_Distinct_Name (Subp_Id : Entity_Id); + -- Ensure that the contract of subprogram Subp_Id does not contain + -- another Test_Case pragma with the same Name as the current one. + + ------------------------- + -- Check_Distinct_Name -- + ------------------------- + + procedure Check_Distinct_Name (Subp_Id : Entity_Id) is + Items : constant Node_Id := Contract (Subp_Id); + Name : constant String_Id := Get_Name_From_CTC_Pragma (N); + Prag : Node_Id; + + begin + -- Inspect all Test_Case pragma of the related subprogram + -- looking for one with a duplicate "Name" argument. + + if Present (Items) then + Prag := Contract_Test_Cases (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Test_Case + and then String_Equal + (Name, Get_Name_From_CTC_Pragma (Prag)) + then + Error_Msg_Sloc := Sloc (Prag); + Error_Pragma ("name for pragma % is already used #"); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end if; + end Check_Distinct_Name; + + -- Local variables + + Pack_Decl : constant Node_Id := Unit (Cunit (Current_Sem_Unit)); + Asp_Arg : Node_Id; + Context : Node_Id; + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; + + -- Start of processing for Test_Case + + begin GNAT_Pragma; - Check_Test_Case; + Check_At_Least_N_Arguments (2); + Check_At_Most_N_Arguments (4); + Check_Arg_Order + ((Name_Name, Name_Mode, Name_Requires, Name_Ensures)); + -- Argument "Name" + + Check_Optional_Identifier (Arg1, Name_Name); + Check_Arg_Is_OK_Static_Expression (Arg1, Standard_String); + + -- Argument "Mode" + + Check_Optional_Identifier (Arg2, Name_Mode); + Check_Arg_Is_One_Of (Arg2, Name_Nominal, Name_Robustness); + + -- Arguments "Requires" and "Ensures" + + if Present (Arg3) then + if Present (Arg4) then + Check_Identifier (Arg3, Name_Requires); + Check_Identifier (Arg4, Name_Ensures); + else + Check_Identifier_Is_One_Of + (Arg3, Name_Requires, Name_Ensures); + end if; + end if; + + -- Pragma Test_Case must be associated with a subprogram declared + -- in a library-level package. First determine whether the current + -- compilation unit is a legal context. + + if Nkind_In (Pack_Decl, N_Package_Declaration, + N_Generic_Package_Declaration) + then + null; + + -- Otherwise the placement is illegal + + else + Pragma_Misplaced; + return; + end if; + + Subp_Decl := Find_Related_Subprogram_Or_Body (N); + + -- Find the enclosing context + + Context := Parent (Subp_Decl); + + if Present (Context) then + Context := Parent (Context); + end if; + + -- Verify the placement of the pragma + + if Nkind (Subp_Decl) = N_Abstract_Subprogram_Declaration then + Error_Pragma + ("pragma % cannot be applied to abstract subprogram"); + return; + + elsif Nkind (Subp_Decl) = N_Entry_Declaration then + Error_Pragma ("pragma % cannot be applied to entry"); + return; + + -- The context is a [generic] subprogram declared at the top level + -- of the [generic] package unit. + + elsif Nkind_In (Subp_Decl, N_Generic_Subprogram_Declaration, + N_Subprogram_Declaration) + and then Present (Context) + and then Nkind_In (Context, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Subp_Id := Defining_Entity (Subp_Decl); + + -- Otherwise the placement is illegal + + else + Pragma_Misplaced; + return; + end if; + + -- Preanalyze the original aspect argument "Name" for ASIS or for + -- a generic subprogram to properly capture global references. + + if ASIS_Mode or else Is_Generic_Subprogram (Subp_Id) then + Asp_Arg := Test_Case_Arg (N, Name_Name, From_Aspect => True); + + if Present (Asp_Arg) then + + -- The argument appears with an identifier in association + -- form. + + if Nkind (Asp_Arg) = N_Component_Association then + Asp_Arg := Expression (Asp_Arg); + end if; + + Check_Expr_Is_OK_Static_Expression + (Asp_Arg, Standard_String); + end if; + end if; + + -- Ensure that the all Test_Case pragmas of the related subprogram + -- have distinct names. + + Check_Distinct_Name (Subp_Id); + + -- Construct a generic template for the pragma when the context is + -- a generic subprogram and the pragma is a source construct. + + Create_Generic_Template (N, Subp_Id); + + -- Fully analyze the pragma when it appears inside a subprogram + -- body because it cannot benefit from forward references. + + if Nkind_In (Subp_Decl, N_Subprogram_Body, + N_Subprogram_Body_Stub) + then + Analyze_Test_Case_In_Decl_Part (N); + end if; + + -- Chain the pragma on the contract for further processing + + Add_Contract_Item (N, Subp_Id); + end Test_Case; + -------------------------- -- Thread_Local_Storage -- -------------------------- @@ -21460,9 +21040,10 @@ raise Program_Error; end if; - Rewrite (N, Make_Pragma (Loc, - Chars => Name_Warnings, - Pragma_Argument_Associations => Shifted_Args)); + Rewrite (N, + Make_Pragma (Loc, + Chars => Name_Warnings, + Pragma_Argument_Associations => Shifted_Args)); Analyze (N); raise Pragma_Exit; end if; @@ -21744,175 +21325,197 @@ -- Analyze_Pre_Post_Condition_In_Decl_Part -- --------------------------------------------- - procedure Analyze_Pre_Post_Condition_In_Decl_Part - (Prag : Node_Id; - Subp_Id : Entity_Id) - is - Arg1 : constant Node_Id := First (Pragma_Argument_Associations (Prag)); - Nam : constant Name_Id := Original_Aspect_Name (Prag); - Expr : Node_Id; + procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id) is + procedure Process_Class_Wide_Condition + (Expr : Node_Id; + Spec_Id : Entity_Id; + Subp_Decl : Node_Id); + -- Replace the type of all references to the controlling formal of + -- subprogram Spec_Id found in expression Expr with the corresponding + -- class-wide type. Subp_Decl is the subprogram [body] declaration + -- where the pragma resides. - Restore_Scope : Boolean := False; - -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit + ---------------------------------- + -- Process_Class_Wide_Condition -- + ---------------------------------- - begin - -- Ensure that the subprogram and its formals are visible when analyzing - -- the expression of the pragma. + procedure Process_Class_Wide_Condition + (Expr : Node_Id; + Spec_Id : Entity_Id; + Subp_Decl : Node_Id) + is + Disp_Typ : constant Entity_Id := Find_Dispatching_Type (Spec_Id); - if not In_Open_Scopes (Subp_Id) then - Restore_Scope := True; - Push_Scope (Subp_Id); - Install_Formals (Subp_Id); - end if; + ACW : Entity_Id := Empty; + -- Access to Disp_Typ'Class, created if there is a controlling formal + -- that is an access parameter. - -- Preanalyze the boolean expression, we treat this as a spec expression - -- (i.e. similar to a default expression). + function Access_Class_Wide_Type return Entity_Id; + -- If expression Expr contains a reference to a controlling access + -- parameter, create an access to Disp_Typ'Class for the necessary + -- conversions if one does not exist. - Expr := Get_Pragma_Arg (Arg1); + function Replace_Type (N : Node_Id) return Traverse_Result; + -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class + -- aspect for a primitive subprogram of a tagged type Disp_Typ, a + -- name that denotes a formal parameter of type Disp_Typ is treated + -- as having type Disp_Typ'Class. Similarly, a name that denotes a + -- formal access parameter of type access-to-Disp_Typ is interpreted + -- as with type access-to-Disp_Typ'Class. This ensures the expression + -- is well defined for a primitive subprogram of a type descended + -- from Disp_Typ. - -- In ASIS mode, for a pragma generated from a source aspect, analyze - -- the original aspect expression, which is shared with the generated - -- pragma. + ---------------------------- + -- Access_Class_Wide_Type -- + ---------------------------- - if ASIS_Mode and then Present (Corresponding_Aspect (Prag)) then - Expr := Expression (Corresponding_Aspect (Prag)); - end if; + function Access_Class_Wide_Type return Entity_Id is + Loc : constant Source_Ptr := Sloc (N); - Preanalyze_Assert_Expression (Expr, Standard_Boolean); + begin + if No (ACW) then + ACW := Make_Temporary (Loc, 'T'); - -- For a class-wide condition, a reference to a controlling formal must - -- be interpreted as having the class-wide type (or an access to such) - -- so that the inherited condition can be properly applied to any - -- overriding operation (see ARM12 6.6.1 (7)). + Insert_Before_And_Analyze (Subp_Decl, + Make_Full_Type_Declaration (Loc, + Defining_Identifier => ACW, + Type_Definition => + Make_Access_To_Object_Definition (Loc, + Subtype_Indication => + New_Occurrence_Of (Class_Wide_Type (Disp_Typ), Loc), + All_Present => True))); - if Class_Present (Prag) then - Class_Wide_Condition : declare - T : constant Entity_Id := Find_Dispatching_Type (Subp_Id); + Freeze_Before (Subp_Decl, ACW); + end if; - ACW : Entity_Id := Empty; - -- Access to T'class, created if there is a controlling formal - -- that is an access parameter. + return ACW; + end Access_Class_Wide_Type; - function Get_ACW return Entity_Id; - -- If the expression has a reference to an controlling access - -- parameter, create an access to T'class for the necessary - -- conversions if one does not exist. + ------------------ + -- Replace_Type -- + ------------------ - function Process (N : Node_Id) return Traverse_Result; - -- ARM 6.1.1: Within the expression for a Pre'Class or Post'Class - -- aspect for a primitive subprogram of a tagged type T, a name - -- that denotes a formal parameter of type T is interpreted as - -- having type T'Class. Similarly, a name that denotes a formal - -- accessparameter of type access-to-T is interpreted as having - -- type access-to-T'Class. This ensures the expression is well- - -- defined for a primitive subprogram of a type descended from T. - -- Note that this replacement is not done for selector names in - -- parameter associations. These carry an entity for reference - -- purposes, but semantically they are just identifiers. + function Replace_Type (N : Node_Id) return Traverse_Result is + Context : constant Node_Id := Parent (N); + Loc : constant Source_Ptr := Sloc (N); + CW_Typ : Entity_Id := Empty; + Ent : Entity_Id; + Typ : Entity_Id; - ------------- - -- Get_ACW -- - ------------- + begin + if Is_Entity_Name (N) + and then Present (Entity (N)) + and then Is_Formal (Entity (N)) + then + Ent := Entity (N); + Typ := Etype (Ent); - function Get_ACW return Entity_Id is - Loc : constant Source_Ptr := Sloc (Prag); - Decl : Node_Id; + -- Do not perform the type replacement for selector names in + -- parameter associations. These carry an entity for reference + -- purposes, but semantically they are just identifiers. - begin - if No (ACW) then - Decl := - Make_Full_Type_Declaration (Loc, - Defining_Identifier => Make_Temporary (Loc, 'T'), - Type_Definition => - Make_Access_To_Object_Definition (Loc, - Subtype_Indication => - New_Occurrence_Of (Class_Wide_Type (T), Loc), - All_Present => True)); + if Nkind (Context) = N_Type_Conversion then + null; - Insert_Before (Unit_Declaration_Node (Subp_Id), Decl); - Analyze (Decl); - ACW := Defining_Identifier (Decl); - Freeze_Before (Unit_Declaration_Node (Subp_Id), ACW); + elsif Nkind (Context) = N_Parameter_Association + and then Selector_Name (Context) = N + then + null; + + elsif Typ = Disp_Typ then + CW_Typ := Class_Wide_Type (Typ); + + elsif Is_Access_Type (Typ) + and then Designated_Type (Typ) = Disp_Typ + then + CW_Typ := Access_Class_Wide_Type; end if; - return ACW; - end Get_ACW; + if Present (CW_Typ) then + Rewrite (N, + Make_Type_Conversion (Loc, + Subtype_Mark => New_Occurrence_Of (CW_Typ, Loc), + Expression => New_Occurrence_Of (Ent, Loc))); + Set_Etype (N, CW_Typ); + end if; + end if; - ------------- - -- Process -- - ------------- + return OK; + end Replace_Type; - function Process (N : Node_Id) return Traverse_Result is - Loc : constant Source_Ptr := Sloc (N); - Typ : Entity_Id; + procedure Replace_Types is new Traverse_Proc (Replace_Type); - begin - if Is_Entity_Name (N) - and then Present (Entity (N)) - and then Is_Formal (Entity (N)) - and then Nkind (Parent (N)) /= N_Type_Conversion - and then - (Nkind (Parent (N)) /= N_Parameter_Association - or else N /= Selector_Name (Parent (N))) - then - if Etype (Entity (N)) = T then - Typ := Class_Wide_Type (T); + -- Local variables - elsif Is_Access_Type (Etype (Entity (N))) - and then Designated_Type (Etype (Entity (N))) = T - then - Typ := Get_ACW; - else - Typ := Empty; - end if; + Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (N); - if Present (Typ) then - Rewrite (N, - Make_Type_Conversion (Loc, - Subtype_Mark => - New_Occurrence_Of (Typ, Loc), - Expression => New_Occurrence_Of (Entity (N), Loc))); - Set_Etype (N, Typ); - end if; + -- Start of processing for Process_Class_Wide_Condition + + begin + -- The subprogram subject to Pre'Class/Post'Class does not have a + -- dispatching type, therefore the aspect/pragma is illegal. + + if No (Disp_Typ) then + if From_Aspect_Specification (N) then + Error_Msg_Name_1 := Prag_Nam; + Error_Msg_N + ("aspect % can only be specified for a primitive operation " + & "of a tagged type", Corresponding_Aspect (N)); + + -- The pragma is a source construct + + else + if Prag_Nam = Name_Precondition then + Error_Msg_Name_1 := Name_Pre_Class; + else + Error_Msg_Name_1 := Name_Post_Class; end if; - return OK; - end Process; + Error_Msg_N + ("pragma % can only be specified for a primitive operation " + & "of a tagged type", N); + end if; + end if; - procedure Replace_Type is new Traverse_Proc (Process); + Replace_Types (Expr); + end Process_Class_Wide_Condition; - -- Start of processing for Class_Wide_Condition + -- Local variables - begin - if not Present (T) then + Subp_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); + Expr : constant Node_Id := + Expression (Get_Argument (N, Defining_Entity (Subp_Decl))); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); - -- Pre'Class/Post'Class aspect cases + Restore_Scope : Boolean := False; + -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit - if From_Aspect_Specification (Prag) then - Error_Msg_Name_1 := Nam; - Error_Msg_N - ("aspect% can only be specified for a primitive " - & "operation of a tagged type", - Corresponding_Aspect (Prag)); + -- Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part - -- Pre_Class, Post_Class pragma cases + begin + -- Ensure that the subprogram and its formals are visible when analyzing + -- the expression of the pragma. - else - if Nam = Name_uPre then - Error_Msg_Name_1 := Name_Pre_Class; - else - Error_Msg_Name_1 := Name_Post_Class; - end if; + if not In_Open_Scopes (Spec_Id) then + Restore_Scope := True; + Push_Scope (Spec_Id); - Error_Msg_N - ("pragma% can only be specified for a primitive " - & "operation of a tagged type", - Corresponding_Aspect (Prag)); - end if; - end if; + if Is_Generic_Subprogram (Spec_Id) then + Install_Generic_Formals (Spec_Id); + else + Install_Formals (Spec_Id); + end if; + end if; - Replace_Type (Get_Pragma_Arg (Arg1)); - end Class_Wide_Condition; + Preanalyze_Assert_Expression (Expr, Standard_Boolean); + + -- For a class-wide condition, a reference to a controlling formal must + -- be interpreted as having the class-wide type (or an access to such) + -- so that the inherited condition can be properly applied to any + -- overriding operation (see ARM12 6.6.1 (7)). + + if Class_Present (N) then + Process_Class_Wide_Condition (Expr, Spec_Id, Subp_Decl); end if; -- Remove the subprogram from the scope stack now that the pre-analysis @@ -22638,8 +22241,7 @@ Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Body_Id : constant Entity_Id := Defining_Entity (Body_Decl); Errors : constant Nat := Serious_Errors_Detected; - Refs : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Refs : constant Node_Id := Expression (Get_Argument (N)); Clause : Node_Id; Deps : Node_Id; Dummy : Boolean; @@ -22665,7 +22267,7 @@ return; end if; - Deps := Get_Pragma_Arg (First (Pragma_Argument_Associations (Depends))); + Deps := Expression (Get_Argument (Depends)); -- A null dependency relation renders the refinement useless because it -- cannot possibly mention abstract states with visible refinement. Note @@ -23509,8 +23111,7 @@ -- Start of processing for Collect_Global_Items begin - Process_Global_List - (Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)))); + Process_Global_List (Expression (Get_Argument (Prag))); end Collect_Global_Items; ------------------------- @@ -23577,8 +23178,7 @@ Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N); Errors : constant Nat := Serious_Errors_Detected; - Items : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Items : constant Node_Id := Expression (Get_Argument (N)); Spec_Id : Entity_Id; -- Start of processing for Analyze_Refined_Global_In_Decl_Part @@ -24493,8 +24093,7 @@ -- Local declarations Body_Decl : constant Node_Id := Parent (N); - Clauses : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (N))); + Clauses : constant Node_Id := Expression (Get_Argument (N)); Clause : Node_Id; -- Start of processing for Analyze_Refined_State_In_Decl_Part @@ -24554,28 +24153,83 @@ -- Analyze_Test_Case_In_Decl_Part -- ------------------------------------ - procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id) is + procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id) is + procedure Preanalyze_Test_Case_Arg + (Arg_Nam : Name_Id; + Subp_Id : Entity_Id); + -- Preanalyze one of the optional arguments "Requires" or "Ensures" + -- denoted by Arg_Nam. Subp_Id is the entity of the subprogram subject + -- to pragma Test_Case. + + ------------------------------ + -- Preanalyze_Test_Case_Arg -- + ------------------------------ + + procedure Preanalyze_Test_Case_Arg + (Arg_Nam : Name_Id; + Subp_Id : Entity_Id) + is + Arg : Node_Id; + + begin + -- Preanalyze the original aspect argument for ASIS or for a generic + -- subprogram to properly capture global references. + + if ASIS_Mode or else Is_Generic_Subprogram (Subp_Id) then + Arg := + Test_Case_Arg + (Prag => N, + Arg_Nam => Arg_Nam, + From_Aspect => True); + + if Present (Arg) then + Preanalyze_Assert_Expression + (Expression (Arg), Standard_Boolean); + end if; + end if; + + Arg := Test_Case_Arg (N, Arg_Nam); + + if Present (Arg) then + Preanalyze_Assert_Expression (Expression (Arg), Standard_Boolean); + end if; + end Preanalyze_Test_Case_Arg; + + -- Local variables + + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; + + Restore_Scope : Boolean := False; + -- Gets set True if we do a Push_Scope needing a Pop_Scope on exit + + -- Start of processing for Analyze_Test_Case_In_Decl_Part + begin - -- Install formals and push subprogram spec onto scope stack so that we - -- can see the formals from the pragma. + Subp_Decl := Find_Related_Subprogram_Or_Body (N); + Subp_Id := Defining_Entity (Subp_Decl); - Push_Scope (S); - Install_Formals (S); + -- Ensure that the formal parameters are visible when analyzing all + -- clauses. This falls out of the general rule of aspects pertaining + -- to subprogram declarations. - -- Preanalyze the boolean expressions, we treat these as spec - -- expressions (i.e. similar to a default expression). + if not In_Open_Scopes (Subp_Id) then + Restore_Scope := True; + Push_Scope (Subp_Id); - if Pragma_Name (N) = Name_Test_Case then - Preanalyze_CTC_Args - (N, - Get_Requires_From_CTC_Pragma (N), - Get_Ensures_From_CTC_Pragma (N)); + if Is_Generic_Subprogram (Subp_Id) then + Install_Generic_Formals (Subp_Id); + else + Install_Formals (Subp_Id); + end if; end if; - -- Remove the subprogram from the scope stack now that the pre-analysis - -- of the expressions in the contract case or test case is done. + Preanalyze_Test_Case_Arg (Name_Requires, Subp_Id); + Preanalyze_Test_Case_Arg (Name_Ensures, Subp_Id); - End_Scope; + if Restore_Scope then + End_Scope; + end if; end Analyze_Test_Case_In_Decl_Part; ---------------- @@ -24615,7 +24269,7 @@ PP : Node_Id; Policy : Name_Id; - Ename : constant Name_Id := Original_Aspect_Name (N); + Ename : constant Name_Id := Original_Aspect_Pragma_Name (N); begin -- No effect if not valid assertion kind name @@ -24955,43 +24609,6 @@ end if; end Check_Missing_Part_Of; - --------------------------------- - -- Check_SPARK_Aspect_For_ASIS -- - --------------------------------- - - procedure Check_SPARK_Aspect_For_ASIS (N : Node_Id) is - Expr : Node_Id; - - begin - if ASIS_Mode and then From_Aspect_Specification (N) then - Expr := Expression (Corresponding_Aspect (N)); - if Nkind (Expr) /= N_Aggregate then - Preanalyze_And_Resolve (Expr); - - else - declare - Comps : constant List_Id := Component_Associations (Expr); - Exprs : constant List_Id := Expressions (Expr); - C : Node_Id; - E : Node_Id; - - begin - E := First (Exprs); - while Present (E) loop - Analyze (E); - Next (E); - end loop; - - C := First (Comps); - while Present (C) loop - Analyze (Expression (C)); - Next (C); - end loop; - end; - end if; - end if; - end Check_SPARK_Aspect_For_ASIS; - ------------------------------------- -- Check_State_And_Constituent_Use -- ------------------------------------- @@ -25242,36 +24859,20 @@ -- Local variables - Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Spec_Id : constant Entity_Id := Corresponding_Spec_Of (Subp_Decl); Clause : Node_Id; Clauses : Node_Id; Depends : Node_Id; Formal : Entity_Id; Global : Node_Id; List : Node_Id; - Spec_Id : Entity_Id; -- Start of processing for Collect_Subprogram_Inputs_Outputs begin Global_Seen := False; - -- Find the entity of the corresponding spec when processing a body - - if Nkind (Subp_Decl) = N_Subprogram_Body - and then Present (Corresponding_Spec (Subp_Decl)) - then - Spec_Id := Corresponding_Spec (Subp_Decl); - - elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub - and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) - then - Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); - - else - Spec_Id := Subp_Id; - end if; - -- Process all formal parameters Formal := First_Formal (Spec_Id); @@ -25316,7 +24917,7 @@ if Present (Global) then Global_Seen := True; - List := Expression (First (Pragma_Argument_Associations (Global))); + List := Expression (Get_Argument (Global, Spec_Id)); -- The pragma may not have been analyzed because of the arbitrary -- declaration order of aspects. Make sure that it is analyzed for @@ -25337,8 +24938,7 @@ -- the inputs and outputs from [Refined_]Depends. elsif Synthesize and then Present (Depends) then - Clauses := - Get_Pragma_Arg (First (Pragma_Argument_Associations (Depends))); + Clauses := Expression (Get_Argument (Depends, Spec_Id)); -- Multiple dependency clauses appear as an aggregate @@ -25367,6 +24967,155 @@ Name_Priority_Specific_Dispatching); end Delay_Config_Pragma_Analyze; + ----------------------- + -- Duplication_Error -- + ----------------------- + + procedure Duplication_Error (Prag : Node_Id; Prev : Node_Id) is + Prag_From_Asp : constant Boolean := From_Aspect_Specification (Prag); + Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag); + Prev_From_Asp : constant Boolean := From_Aspect_Specification (Prev); + + begin + Error_Msg_Sloc := Sloc (Prev); + + -- Emit a precise message to distinguish between source pragmas and + -- pragmas generated from aspects. The ordering of the two pragmas is + -- the following: + + -- Prev -- ok + -- Prag -- duplicate + + -- No error is emitted when both pragmas come from aspects because this + -- is already detected by the general aspect analysis mechanism. + + if Prag_Nam = Name_uPre then + Error_Msg_Name_1 := Name_Pre; + elsif Prag_Nam = Name_uPost then + Error_Msg_Name_1 := Name_Post; + else + Error_Msg_Name_1 := Prag_Nam; + end if; + + -- The item appears as aspect XXX'Class or pragma XXX_Class + + if Class_Present (Prag) then + if Prag_From_Asp and Prev_From_Asp then + null; + elsif Prag_From_Asp then + Error_Msg_N + ("aspect `%'Class` duplicates pragma declared #", Prag); + elsif Prev_From_Asp then + Error_Msg_N + ("pragma `%_Class` duplicates aspect declared #", Prag); + else + Error_Msg_N + ("pragma `%_Class` duplicates pragma declared #", Prag); + end if; + + -- Otherwise the pragma appears in its normal form + + else + if Prag_From_Asp and Prev_From_Asp then + null; + elsif Prag_From_Asp then + Error_Msg_N ("aspect % duplicates pragma declared #", Prag); + elsif Prev_From_Asp then + Error_Msg_N ("pragma % duplicates aspect declared #", Prag); + else + Error_Msg_N ("pragma % duplicates pragma declared #", Prag); + end if; + end if; + end Duplication_Error; + + ---------------------------------- + -- Find_Related_Package_Or_Body -- + ---------------------------------- + + function Find_Related_Package_Or_Body + (Prag : Node_Id; + Do_Checks : Boolean := False) return Node_Id + is + Context : constant Node_Id := Parent (Prag); + Prag_Nam : constant Name_Id := Pragma_Name (Prag); + Stmt : Node_Id; + + begin + Stmt := Prev (Prag); + while Present (Stmt) loop + + -- Skip prior pragmas, but check for duplicates + + if Nkind (Stmt) = N_Pragma then + if Do_Checks and then Pragma_Name (Stmt) = Prag_Nam then + Duplication_Error + (Prag => Prag, + Prev => Stmt); + end if; + + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + if Nkind (Stmt) = N_Subprogram_Declaration then + + -- The subprogram declaration is an internally generated spec + -- for an expression function. + + if Nkind (Original_Node (Stmt)) = N_Expression_Function then + return Stmt; + + -- The subprogram is actually an instance housed within an + -- anonymous wrapper package. + + elsif Present (Generic_Parent (Specification (Stmt))) then + return Stmt; + end if; + end if; + + -- Return the current source construct which is illegal + + else + return Stmt; + end if; + + Prev (Stmt); + end loop; + + -- If we fall through, then the pragma was either the first declaration + -- or it was preceded by other pragmas and no source constructs. + + -- The pragma is associated with a package. The immediate context in + -- this case is the specification of the package. + + if Nkind (Context) = N_Package_Specification then + return Parent (Context); + + -- The pragma appears in the declarations of a package body + + elsif Nkind (Context) = N_Package_Body then + return Context; + + -- The pragma appears in the statements of a package body + + elsif Nkind (Context) = N_Handled_Sequence_Of_Statements + and then Nkind (Parent (Context)) = N_Package_Body + then + return Parent (Context); + + -- The pragma is a byproduct of aspect expansion, return the related + -- context of the original aspect. This case has a lower priority as + -- the above circuitry pinpoints precisely the related context. + + elsif Present (Corresponding_Aspect (Prag)) then + return Parent (Corresponding_Aspect (Prag)); + + -- No candidate packge [body] found + + else + return Empty; + end if; + end Find_Related_Package_Or_Body; + ------------------------------------- -- Find_Related_Subprogram_Or_Body -- ------------------------------------- @@ -25375,42 +25124,63 @@ (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id is - Context : constant Node_Id := Parent (Prag); - Nam : constant Name_Id := Pragma_Name (Prag); - Stmt : Node_Id; + Prag_Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag); - Look_For_Body : constant Boolean := - Nam_In (Nam, Name_Refined_Depends, - Name_Refined_Global, - Name_Refined_Post); - -- Refinement pragmas must be associated with a subprogram body [stub] + procedure Expression_Function_Error; + -- Emit an error concerning pragma Prag that illegaly applies to an + -- expression function. - begin - pragma Assert (Nkind (Prag) = N_Pragma); + ------------------------------- + -- Expression_Function_Error -- + ------------------------------- - -- If the pragma is a byproduct of aspect expansion, return the related - -- context of the original aspect. + procedure Expression_Function_Error is + begin + Error_Msg_Name_1 := Prag_Nam; - if Present (Corresponding_Aspect (Prag)) then - return Parent (Corresponding_Aspect (Prag)); - end if; + -- Emit a precise message to distinguish between source pragmas and + -- pragmas generated from aspects. - -- Otherwise the pragma is a source construct, most likely part of a - -- declarative list. Skip preceding declarations while looking for a - -- proper subprogram declaration. + if From_Aspect_Specification (Prag) then + Error_Msg_N + ("aspect % cannot apply to a stand alone expression function", + Prag); + else + Error_Msg_N + ("pragma % cannot apply to a stand alone expression function", + Prag); + end if; + end Expression_Function_Error; - pragma Assert (Is_List_Member (Prag)); + -- Local variables + Context : constant Node_Id := Parent (Prag); + Stmt : Node_Id; + + Look_For_Body : constant Boolean := + Nam_In (Prag_Nam, Name_Refined_Depends, + Name_Refined_Global, + Name_Refined_Post); + -- Refinement pragmas must be associated with a subprogram body [stub] + + -- Start of processing for Find_Related_Subprogram_Or_Body + + begin Stmt := Prev (Prag); while Present (Stmt) loop - -- Skip prior pragmas, but check for duplicates + -- Skip prior pragmas, but check for duplicates. Pragmas produced + -- by splitting a complex pre/postcondition are not considered to + -- be duplicates. if Nkind (Stmt) = N_Pragma then - if Do_Checks and then Pragma_Name (Stmt) = Nam then - Error_Msg_Name_1 := Nam; - Error_Msg_Sloc := Sloc (Stmt); - Error_Msg_N ("pragma % duplicates pragma declared #", Prag); + if Do_Checks + and then not Split_PPC (Stmt) + and then Original_Aspect_Pragma_Name (Stmt) = Prag_Nam + then + Duplication_Error + (Prag => Prag, + Prev => Stmt); end if; -- Emit an error when a refinement pragma appears on an expression @@ -25422,11 +25192,7 @@ and then Nkind (Original_Node (Stmt)) = N_Expression_Function and then not Has_Completion (Defining_Entity (Stmt)) then - Error_Msg_Name_1 := Nam; - Error_Msg_N - ("pragma % cannot apply to a stand alone expression function", - Prag); - + Expression_Function_Error; return Empty; -- The refinement pragma applies to a subprogram body stub @@ -25439,8 +25205,22 @@ -- Skip internally generated code elsif not Comes_From_Source (Stmt) then - null; + if Nkind (Stmt) = N_Subprogram_Declaration then + -- The subprogram declaration is an internally generated spec + -- for an expression function. + + if Nkind (Original_Node (Stmt)) = N_Expression_Function then + return Stmt; + + -- The subprogram is actually an instance housed within an + -- anonymous wrapper package. + + elsif Present (Generic_Parent (Specification (Stmt))) then + return Stmt; + end if; + end if; + -- Return the current construct which is either a subprogram body, -- a subprogram declaration or is illegal. @@ -25459,11 +25239,24 @@ if Nkind (Context) = N_Compilation_Unit_Aux then return Unit (Parent (Context)); + -- The pragma appears inside the statements of a subprogram body. This + -- placement is the result of subprogram contract expansion. + + elsif Nkind (Context) = N_Handled_Sequence_Of_Statements then + return Parent (Context); + -- The pragma appears inside the declarative part of a subprogram body elsif Nkind (Context) = N_Subprogram_Body then return Context; + -- The pragma is a byproduct of aspect expansion, return the related + -- context of the original aspect. This case has a lower priority as + -- the above circuitry pinpoints precisely the related context. + + elsif Present (Corresponding_Aspect (Prag)) then + return Parent (Corresponding_Aspect (Prag)); + -- No candidate subprogram [body] found else @@ -25471,6 +25264,39 @@ end if; end Find_Related_Subprogram_Or_Body; + ------------------ + -- Get_Argument -- + ------------------ + + function Get_Argument + (Prag : Node_Id; + Spec_Id : Entity_Id := Empty) return Node_Id + is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + + begin + -- Use the expression of the original aspect if possible when compiling + -- for ASIS or when analyzing the template of a generic subprogram. In + -- both cases the aspect's tree must be decorated to allow for ASIS + -- queries or to save all global references in the generic context. + + if From_Aspect_Specification (Prag) + and then + (ASIS_Mode or else (Present (Spec_Id) + and then Is_Generic_Subprogram (Spec_Id))) + then + return Corresponding_Aspect (Prag); + + -- Otherwise use the expression of the pragma + + elsif Present (Args) then + return First (Args); + + else + return Empty; + end if; + end Get_Argument; + ------------------------- -- Get_Base_Subprogram -- ------------------------- @@ -26191,118 +26017,6 @@ end case; end Is_Valid_Assertion_Kind; - ----------------------------------------- - -- Make_Aspect_For_PPC_In_Gen_Sub_Decl -- - ----------------------------------------- - - procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id) is - Aspects : constant List_Id := New_List; - Loc : constant Source_Ptr := Sloc (Decl); - Or_Decl : constant Node_Id := Original_Node (Decl); - - Original_Aspects : List_Id; - -- To capture global references, a copy of the created aspects must be - -- inserted in the original tree. - - Prag : Node_Id; - Prag_Arg_Ass : Node_Id; - Prag_Id : Pragma_Id; - - begin - -- Check for any PPC pragmas that appear within Decl - - Prag := Next (Decl); - while Nkind (Prag) = N_Pragma loop - Prag_Id := Get_Pragma_Id (Chars (Pragma_Identifier (Prag))); - - case Prag_Id is - when Pragma_Postcondition | Pragma_Precondition => - Prag_Arg_Ass := First (Pragma_Argument_Associations (Prag)); - - -- Make an aspect from any PPC pragma - - Append_To (Aspects, - Make_Aspect_Specification (Loc, - Identifier => - Make_Identifier (Loc, Chars (Pragma_Identifier (Prag))), - Expression => - Copy_Separate_Tree (Expression (Prag_Arg_Ass)))); - - -- Generate the analysis information in the pragma expression - -- and then set the pragma node analyzed to avoid any further - -- analysis. - - Analyze (Expression (Prag_Arg_Ass)); - Set_Analyzed (Prag, True); - - when others => null; - end case; - - Next (Prag); - end loop; - - -- Set all new aspects into the generic declaration node - - if Is_Non_Empty_List (Aspects) then - - -- Create the list of aspects to be inserted in the original tree - - Original_Aspects := Copy_Separate_List (Aspects); - - -- Check if Decl already has aspects - - -- Attach the new lists of aspects to both the generic copy and the - -- original tree. - - if Has_Aspects (Decl) then - Append_List (Aspects, Aspect_Specifications (Decl)); - Append_List (Original_Aspects, Aspect_Specifications (Or_Decl)); - - else - Set_Parent (Aspects, Decl); - Set_Aspect_Specifications (Decl, Aspects); - Set_Parent (Original_Aspects, Or_Decl); - Set_Aspect_Specifications (Or_Decl, Original_Aspects); - end if; - end if; - end Make_Aspect_For_PPC_In_Gen_Sub_Decl; - - ------------------------- - -- Preanalyze_CTC_Args -- - ------------------------- - - procedure Preanalyze_CTC_Args (N, Arg_Req, Arg_Ens : Node_Id) is - begin - -- Preanalyze the boolean expressions, we treat these as spec - -- expressions (i.e. similar to a default expression). - - if Present (Arg_Req) then - Preanalyze_Assert_Expression - (Get_Pragma_Arg (Arg_Req), Standard_Boolean); - - -- In ASIS mode, for a pragma generated from a source aspect, also - -- analyze the original aspect expression. - - if ASIS_Mode and then Present (Corresponding_Aspect (N)) then - Preanalyze_Assert_Expression - (Original_Node (Get_Pragma_Arg (Arg_Req)), Standard_Boolean); - end if; - end if; - - if Present (Arg_Ens) then - Preanalyze_Assert_Expression - (Get_Pragma_Arg (Arg_Ens), Standard_Boolean); - - -- In ASIS mode, for a pragma generated from a source aspect, also - -- analyze the original aspect expression. - - if ASIS_Mode and then Present (Corresponding_Aspect (N)) then - Preanalyze_Assert_Expression - (Original_Node (Get_Pragma_Arg (Arg_Ens)), Standard_Boolean); - end if; - end if; - end Preanalyze_CTC_Args; - -------------------------------------- -- Process_Compilation_Unit_Pragmas -- -------------------------------------- @@ -26701,4 +26415,100 @@ Generate_Reference (Entity (With_Item), N, Set_Ref => False); end Set_Elab_Unit_Name; + ------------------- + -- Test_Case_Arg -- + ------------------- + + function Test_Case_Arg + (Prag : Node_Id; + Arg_Nam : Name_Id; + From_Aspect : Boolean := False) return Node_Id + is + Aspect : constant Node_Id := Corresponding_Aspect (Prag); + Arg : Node_Id; + Args : Node_Id; + + begin + pragma Assert (Nam_In (Arg_Nam, Name_Ensures, + Name_Mode, + Name_Name, + Name_Requires)); + + -- The caller requests the aspect argument + + if From_Aspect then + if Present (Aspect) + and then Nkind (Expression (Aspect)) = N_Aggregate + then + Args := Expression (Aspect); + + -- "Name" and "Mode" may appear without an identifier as a + -- positional association. + + if Present (Expressions (Args)) then + Arg := First (Expressions (Args)); + + if Present (Arg) and then Arg_Nam = Name_Name then + return Arg; + end if; + + -- Skip "Name" + + Arg := Next (Arg); + + if Present (Arg) and then Arg_Nam = Name_Mode then + return Arg; + end if; + end if; + + -- Some or all arguments may appear as component associatons + + if Present (Component_Associations (Args)) then + Arg := First (Component_Associations (Args)); + while Present (Arg) loop + if Chars (First (Choices (Arg))) = Arg_Nam then + return Arg; + end if; + + Next (Arg); + end loop; + end if; + end if; + + -- Otherwise retrieve the argument directly from the pragma + + else + Arg := First (Pragma_Argument_Associations (Prag)); + + if Present (Arg) and then Arg_Nam = Name_Name then + return Arg; + end if; + + -- Skip argument "Name" + + Arg := Next (Arg); + + if Present (Arg) and then Arg_Nam = Name_Mode then + return Arg; + end if; + + -- Skip argument "Mode" + + Arg := Next (Arg); + + -- Arguments "Requires" and "Ensures" are optional and may not be + -- present at all. + + while Present (Arg) loop + if Chars (Arg) = Arg_Nam then + return Arg; + end if; + + Next (Arg); + end loop; + end if; + + return Empty; + end Test_Case_Arg; + end Sem_Prag; Index: sem_prag.ads =================================================================== --- sem_prag.ads (revision 221098) +++ sem_prag.ads (working copy) @@ -103,14 +103,9 @@ procedure Analyze_Initializes_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Initializes - procedure Analyze_Pre_Post_Condition_In_Decl_Part - (Prag : Node_Id; - Subp_Id : Entity_Id); - -- Perform preanalysis of a [refined] precondition or postcondition that - -- appears on a subprogram declaration or body [stub]. Prag denotes the - -- pragma, Subp_Id is the entity of the related subprogram. The preanalysis - -- of the expression is done as "spec expression" (see section "Handling - -- of Default and Per-Object Expressions in Sem). + procedure Analyze_Pre_Post_Condition_In_Decl_Part (N : Node_Id); + -- Perform preanalysis of [refined] precondition or postcondition pragma + -- N that appears on a subprogram declaration or body [stub]. procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id); -- Preform full analysis of delayed pragma Refined_Depends. This routine @@ -125,12 +120,8 @@ procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id); -- Perform full analysis of delayed pragma Refined_State - procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id); - -- Perform preanalysis of pragma Test_Case that applies to a subprogram - -- declaration. Parameter N denotes the pragma, S is the entity of the - -- related subprogram. The preanalysis of the expression is done as "spec - -- expression" (see section "Handling of Default and Per-Object Expressions - -- in Sem). + procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id); + -- Perform preanalysis of pragma Test_Case procedure Check_Applicable_Policy (N : Node_Id); -- N is either an N_Aspect or an N_Pragma node. There are two cases. If @@ -199,6 +190,23 @@ -- True have their analysis delayed until after the main program is parsed -- and analyzed. + function Find_Related_Subprogram_Or_Body + (Prag : Node_Id; + Do_Checks : Boolean := False) return Node_Id; + -- Subsidiary to the analysis of pragmas Contract_Cases, Depends, Global, + -- Refined_Depends, Refined_Global and Refined_Post and attribute 'Result. + -- Find the declaration of the related subprogram [body or stub] subject + -- to pragma Prag. If flag Do_Checks is set, the routine reports duplicate + -- pragmas and detects improper use of refinement pragmas in stand alone + -- expression functions. The returned value depends on the related pragma + -- as follows: + -- 1) Pragmas Contract_Cases, Depends and Global yield the corresponding + -- N_Subprogram_Declaration node or if the pragma applies to a stand + -- alone body, the N_Subprogram_Body node or Empty if illegal. + -- 2) Pragmas Refined_Depends, Refined_Global and Refined_Post yield + -- N_Subprogram_Body or N_Subprogram_Body_Stub nodes or Empty if + -- illegal. + function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type; -- Given a pragma SPARK_Mode node, return corresponding mode id @@ -247,12 +255,6 @@ -- Name_uInvariant, and Name_uType_Invariant (_Pre, _Post, _Invariant, -- and _Type_Invariant). - procedure Make_Aspect_For_PPC_In_Gen_Sub_Decl (Decl : Node_Id); - -- This routine makes aspects from precondition or postcondition pragmas - -- that appear within a generic subprogram declaration. Decl is the generic - -- subprogram declaration node. Note that the aspects are attached to the - -- generic copy and also to the orginal tree. - procedure Process_Compilation_Unit_Pragmas (N : Node_Id); -- Called at the start of processing compilation unit N to deal with any -- special issues regarding pragmas. In particular, we have to deal with @@ -276,4 +278,23 @@ -- the value of the Interface_Name. Otherwise it is encoded as needed by -- particular operating systems. See the body for details of the encoding. + function Test_Case_Arg + (Prag : Node_Id; + Arg_Nam : Name_Id; + From_Aspect : Boolean := False) return Node_Id; + -- Obtain argument "Name", "Mode", "Ensures" or "Requires" from Test_Case + -- pragma Prag as denoted by Arg_Nam. When From_Aspect is set, an attempt + -- is made to retrieve the argument from the corresponding aspect if there + -- is one. The returned argument has several formats: + -- + -- N_Pragma_Argument_Association if retrieved directly from the pragma + -- + -- N_Component_Association if retrieved from the corresponding aspect and + -- the argument appears in a named association form. + -- + -- An arbitrary expression if retrieved from the corresponding aspect and + -- the argument appears in positional form. + -- + -- Empty if there is no such argument + end Sem_Prag; Index: sem_ch12.adb =================================================================== --- sem_ch12.adb (revision 221098) +++ sem_ch12.adb (working copy) @@ -59,7 +59,6 @@ with Sem_Elab; use Sem_Elab; with Sem_Elim; use Sem_Elim; with Sem_Eval; use Sem_Eval; -with Sem_Prag; use Sem_Prag; with Sem_Res; use Sem_Res; with Sem_Type; use Sem_Type; with Sem_Util; use Sem_Util; @@ -3073,9 +3072,8 @@ Start_Generic; Enter_Name (Id); - Set_Ekind (Id, E_Generic_Package); - Set_Etype (Id, Standard_Void_Type); - Set_Contract (Id, Make_Contract (Sloc (Id))); + Set_Ekind (Id, E_Generic_Package); + Set_Etype (Id, Standard_Void_Type); -- A generic package declared within a Ghost region is rendered Ghost -- (SPARK RM 6.9(2)). @@ -3170,12 +3168,12 @@ -------------------------------------------- procedure Analyze_Generic_Subprogram_Declaration (N : Node_Id) is - Spec : Node_Id; + Formals : List_Id; Id : Entity_Id; - Formals : List_Id; New_N : Node_Id; Result_Type : Entity_Id; Save_Parent : Node_Id; + Spec : Node_Id; Typ : Entity_Id; begin @@ -3206,7 +3204,6 @@ Spec := Specification (N); Id := Defining_Entity (Spec); Generate_Definition (Id); - Set_Contract (Id, Make_Contract (Sloc (Id))); if Nkind (Id) = N_Defining_Operator_Symbol then Error_Msg_N @@ -3311,17 +3308,14 @@ Set_Categorization_From_Pragmas (N); Validate_Categorization_Dependency (N, Id); + -- Capture all global references that occur within the profile of the + -- generic subprogram. Aspects are not part of this processing because + -- they must be delayed. If processed now, Save_Global_References will + -- destroy the Associated_Node links and prevent the capture of global + -- references when the contract of the generic subprogram is analyzed. + Save_Global_References (Original_Node (N)); - -- For ASIS purposes, convert any postcondition, precondition pragmas - -- into aspects, if N is not a compilation unit by itself, in order to - -- enable the analysis of expressions inside the corresponding PPC - -- pragmas. - - if ASIS_Mode and then Is_List_Member (N) then - Make_Aspect_For_PPC_In_Gen_Sub_Decl (N); - end if; - End_Generic; End_Scope; Exit_Generic_Scope (Id); @@ -4626,6 +4620,10 @@ -- aspects that appear in the generic. This renaming declaration is -- inserted after the instance declaration which it renames. + procedure Instantiate_Contract (Subp_Id : Entity_Id); + -- Instantiate all source pragmas found in the contract of subprogram + -- Subp_Id. The instantiated pragmas are added to list Renaming_List. + ------------------------------------ -- Analyze_Instance_And_Renamings -- ------------------------------------ @@ -4658,11 +4656,12 @@ Suffix_Index => Source_Offset (Sloc (Def_Ent)))); end if; - Pack_Decl := Make_Package_Declaration (Loc, - Specification => Make_Package_Specification (Loc, - Defining_Unit_Name => Pack_Id, - Visible_Declarations => Renaming_List, - End_Label => Empty)); + Pack_Decl := + Make_Package_Declaration (Loc, + Specification => Make_Package_Specification (Loc, + Defining_Unit_Name => Pack_Id, + Visible_Declarations => Renaming_List, + End_Label => Empty)); Set_Instance_Spec (N, Pack_Decl); Set_Is_Generic_Instance (Pack_Id); @@ -4826,6 +4825,62 @@ end if; end Build_Subprogram_Renaming; + -------------------------- + -- Instantiate_Contract -- + -------------------------- + + procedure Instantiate_Contract (Subp_Id : Entity_Id) is + procedure Instantiate_Pragmas (First_Prag : Node_Id); + -- Instantiate all contract-related source pragmas found in the list + -- starting with pragma First_Prag. Each instantiated pragma is added + -- to list Renaming_List. + + ------------------------- + -- Instantiate_Pragmas -- + ------------------------- + + procedure Instantiate_Pragmas (First_Prag : Node_Id) is + Inst_Prag : Node_Id; + Prag : Node_Id; + + begin + Prag := First_Prag; + while Present (Prag) loop + if Comes_From_Source (Prag) + and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases, + Name_Depends, + Name_Extensions_Visible, + Name_Global, + Name_Postcondition, + Name_Precondition, + Name_Test_Case) + then + Inst_Prag := + Copy_Generic_Node + (Original_Node (Prag), Empty, Instantiating => True); + + Set_Analyzed (Inst_Prag, False); + Append_To (Renaming_List, Inst_Prag); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end Instantiate_Pragmas; + + -- Local variables + + Items : constant Node_Id := Contract (Subp_Id); + + -- Start of processing for Instantiate_Contract + + begin + if Present (Items) then + Instantiate_Pragmas (Pre_Post_Conditions (Items)); + Instantiate_Pragmas (Contract_Test_Cases (Items)); + Instantiate_Pragmas (Classifications (Items)); + end if; + end Instantiate_Contract; + -- Local variables Save_IPSM : constant Boolean := Ignore_Pragma_SPARK_Mode; @@ -4991,7 +5046,9 @@ end if; Append (Act_Decl, Renaming_List); + Instantiate_Contract (Gen_Unit); Build_Subprogram_Renaming; + Analyze_Instance_And_Renamings; -- If the generic is marked Import (Intrinsic), then so is the @@ -5022,9 +5079,6 @@ end if; Generate_Definition (Act_Decl_Id); - -- Set_Contract (Anon_Id, Make_Contract (Sloc (Anon_Id))); - -- ??? needed? - Set_Contract (Act_Decl_Id, Make_Contract (Sloc (Act_Decl_Id))); -- Inherit all inlining-related flags which apply to the generic in -- the subprogram and its declaration. @@ -10743,30 +10797,30 @@ (Body_Info : Pending_Body_Info; Body_Optional : Boolean := False) is - Act_Decl : constant Node_Id := Body_Info.Act_Decl; - Inst_Node : constant Node_Id := Body_Info.Inst_Node; - Loc : constant Source_Ptr := Sloc (Inst_Node); - Gen_Id : constant Node_Id := Name (Inst_Node); - Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node); - Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); - Anon_Id : constant Entity_Id := - Defining_Unit_Name (Specification (Act_Decl)); - Pack_Id : constant Entity_Id := - Defining_Unit_Name (Parent (Act_Decl)); - Gen_Body : Node_Id; - Gen_Body_Id : Node_Id; - Act_Body : Node_Id; - Pack_Body : Node_Id; - Ret_Expr : Node_Id; + Act_Decl : constant Node_Id := Body_Info.Act_Decl; + Inst_Node : constant Node_Id := Body_Info.Inst_Node; + Loc : constant Source_Ptr := Sloc (Inst_Node); + Gen_Id : constant Node_Id := Name (Inst_Node); + Gen_Unit : constant Entity_Id := Get_Generic_Entity (Inst_Node); + Gen_Decl : constant Node_Id := Unit_Declaration_Node (Gen_Unit); + Anon_Id : constant Entity_Id := + Defining_Unit_Name (Specification (Act_Decl)); + Pack_Id : constant Entity_Id := + Defining_Unit_Name (Parent (Act_Decl)); - Parent_Installed : Boolean := False; - Saved_Style_Check : constant Boolean := Style_Check; Saved_Warnings : constant Warning_Record := Save_Warnings; - Par_Ent : Entity_Id := Empty; - Par_Vis : Boolean := False; + Act_Body : Node_Id; + Gen_Body : Node_Id; + Gen_Body_Id : Node_Id; + Pack_Body : Node_Id; + Par_Ent : Entity_Id := Empty; + Par_Vis : Boolean := False; + Ret_Expr : Node_Id; + Parent_Installed : Boolean := False; + begin Gen_Body_Id := Corresponding_Body (Gen_Decl); @@ -14314,23 +14368,14 @@ end; end if; - -- If a node has aspects, references within their expressions must - -- be saved separately, given they are not directly in the tree. + -- Save all global references found within the aspects of the related + -- node. This is not done for generic subprograms because the aspects + -- must be delayed and analyzed at the end of the declarative part. + -- Only then can global references be saved. This action is performed + -- by the analysis of the generic subprogram contract. - if Has_Aspects (N) then - declare - Aspect : Node_Id; - - begin - Aspect := First (Aspect_Specifications (N)); - while Present (Aspect) loop - if Present (Expression (Aspect)) then - Save_Global_References (Expression (Aspect)); - end if; - - Next (Aspect); - end loop; - end; + if Nkind (N) /= N_Generic_Subprogram_Declaration then + Save_Global_References_In_Aspects (N); end if; end Save_References; @@ -14352,6 +14397,29 @@ Save_References (N); end Save_Global_References; + --------------------------------------- + -- Save_Global_References_In_Aspects -- + --------------------------------------- + + procedure Save_Global_References_In_Aspects (N : Node_Id) is + Asp : Node_Id; + Expr : Node_Id; + + begin + if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then + Asp := First (Aspect_Specifications (N)); + while Present (Asp) loop + Expr := Expression (Asp); + + if Present (Expr) then + Save_Global_References (Expr); + end if; + + Next (Asp); + end loop; + end if; + end Save_Global_References_In_Aspects; + -------------------------------------- -- Set_Copied_Sloc_For_Inlined_Body -- -------------------------------------- Index: sem_ch12.ads =================================================================== --- sem_ch12.ads (revision 221098) +++ sem_ch12.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -152,6 +152,9 @@ -- restored in stack-like fashion. Front-end inlining also uses these -- structures for the management of private/full views. + procedure Save_Global_References_In_Aspects (N : Node_Id); + -- Save all global references in the aspect specifications of node N + procedure Set_Copied_Sloc_For_Inlined_Body (N : Node_Id; E : Entity_Id); -- This procedure is used when a subprogram body is inlined. This process -- shares the same circuitry as the creation of an instantiated copy of Index: sem_util.adb =================================================================== --- sem_util.adb (revision 221098) +++ sem_util.adb (working copy) @@ -47,6 +47,7 @@ with Sem; use Sem; with Sem_Aux; use Sem_Aux; with Sem_Attr; use Sem_Attr; +with Sem_Ch6; use Sem_Ch6; with Sem_Ch8; use Sem_Ch8; with Sem_Ch13; use Sem_Ch13; with Sem_Disp; use Sem_Disp; @@ -250,7 +251,7 @@ ----------------------- procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id) is - Items : constant Node_Id := Contract (Id); + Items : Node_Id := Contract (Id); procedure Add_Classification; -- Prepend Prag to the list of classifications @@ -293,20 +294,23 @@ -- Local variables - Nam : Name_Id; - PPC : Node_Id; + Prag_Nam : Name_Id; -- Start of processing for Add_Contract_Item begin - -- The related context must have a contract and the item to be added - -- must be a pragma. + -- A contract must contain only pragmas - pragma Assert (Present (Items)); pragma Assert (Nkind (Prag) = N_Pragma); + Prag_Nam := Pragma_Name (Prag); - Nam := Original_Aspect_Name (Prag); + -- Create a new contract when adding the first item + if No (Items) then + Items := Make_Contract (Sloc (Id)); + Set_Contract (Id, Items); + end if; + -- Contract items related to [generic] packages or instantiations. The -- applicable pragmas are: -- Abstract_States @@ -315,15 +319,15 @@ -- Part_Of (instantiation only) if Ekind_In (Id, E_Generic_Package, E_Package) then - if Nam_In (Nam, Name_Abstract_State, - Name_Initial_Condition, - Name_Initializes) + if Nam_In (Prag_Nam, Name_Abstract_State, + Name_Initial_Condition, + Name_Initializes) then Add_Classification; -- Indicator Part_Of must be associated with a package instantiation - elsif Nam = Name_Part_Of and then Is_Generic_Instance (Id) then + elsif Prag_Nam = Name_Part_Of and then Is_Generic_Instance (Id) then Add_Classification; -- The pragma is not a proper contract item @@ -336,7 +340,7 @@ -- Refined_States elsif Ekind (Id) = E_Package_Body then - if Nam = Name_Refined_State then + if Prag_Nam = Name_Refined_State then Add_Classification; -- The pragma is not a proper contract item @@ -351,9 +355,7 @@ -- Depends -- Extensions_Visible -- Global - -- Post -- Postcondition - -- Pre -- Precondition -- Test_Case @@ -361,47 +363,15 @@ or else Is_Generic_Subprogram (Id) or else Is_Subprogram (Id) then - if Nam_In (Nam, Name_Pre, - Name_Precondition, - Name_uPre, - Name_Post, - Name_Postcondition, - Name_uPost) - then - -- Before we add a precondition or postcondition to the list, make - -- sure we do not have a disallowed duplicate, which can happen if - -- we use a pragma for Pre[_Class] or Post[_Class] instead of the - -- corresponding aspect. - - if not From_Aspect_Specification (Prag) - and then Nam_In (Nam, Name_Pre, - Name_uPre, - Name_Post, - Name_Post_Class) - then - PPC := Pre_Post_Conditions (Items); - while Present (PPC) loop - if not Split_PPC (PPC) - and then Original_Aspect_Name (PPC) = Nam - then - Error_Msg_Sloc := Sloc (PPC); - Error_Msg_NE - ("duplication of aspect for & given#", Prag, Id); - return; - end if; - - PPC := Next_Pragma (PPC); - end loop; - end if; - + if Nam_In (Prag_Nam, Name_Postcondition, Name_Precondition) then Add_Pre_Post_Condition; - elsif Nam_In (Nam, Name_Contract_Cases, Name_Test_Case) then + elsif Nam_In (Prag_Nam, Name_Contract_Cases, Name_Test_Case) then Add_Contract_Test_Case; - elsif Nam_In (Nam, Name_Depends, - Name_Extensions_Visible, - Name_Global) + elsif Nam_In (Prag_Nam, Name_Depends, + Name_Extensions_Visible, + Name_Global) then Add_Classification; @@ -412,15 +382,20 @@ end if; -- Contract items related to subprogram bodies. Applicable pragmas are: + -- Postcondition + -- Precondition -- Refined_Depends -- Refined_Global -- Refined_Post elsif Ekind (Id) = E_Subprogram_Body then - if Nam_In (Nam, Name_Refined_Depends, Name_Refined_Global) then + if Nam_In (Prag_Nam, Name_Refined_Depends, Name_Refined_Global) then Add_Classification; - elsif Nam = Name_Refined_Post then + elsif Nam_In (Prag_Nam, Name_Postcondition, + Name_Precondition, + Name_Refined_Post) + then Add_Pre_Post_Condition; -- The pragma is not a proper contract item @@ -437,11 +412,11 @@ -- Part_Of elsif Ekind (Id) = E_Variable then - if Nam_In (Nam, Name_Async_Readers, - Name_Async_Writers, - Name_Effective_Reads, - Name_Effective_Writes, - Name_Part_Of) + if Nam_In (Prag_Nam, Name_Async_Readers, + Name_Async_Writers, + Name_Effective_Reads, + Name_Effective_Writes, + Name_Part_Of) then Add_Classification; @@ -3047,169 +3022,326 @@ -- Check_Result_And_Post_State -- --------------------------------- - procedure Check_Result_And_Post_State - (Prag : Node_Id; - Result_Seen : in out Boolean) - is - procedure Check_Expression (Expr : Node_Id); - -- Perform the 'Result and post-state checks on a given expression + procedure Check_Result_And_Post_State (Subp_Id : Entity_Id) is + procedure Check_Result_And_Post_State_In_Pragma + (Prag : Node_Id; + Result_Seen : in out Boolean); + -- Determine whether pragma Prag mentions attribute 'Result and whether + -- the pragma contains an expression that evaluates differently in pre- + -- and post-state. Prag is a [refined] postcondition or a contract-cases + -- pragma. Result_Seen is set when the pragma mentions attribute 'Result - function Is_Function_Result (N : Node_Id) return Traverse_Result; - -- Attempt to find attribute 'Result in a subtree denoted by N + function Has_In_Out_Parameter (Subp_Id : Entity_Id) return Boolean; + -- Determine whether subprogram Subp_Id contains at least one IN OUT + -- formal parameter. - function Is_Trivial_Boolean (N : Node_Id) return Boolean; - -- Determine whether source node N denotes "True" or "False" + ------------------------------------------- + -- Check_Result_And_Post_State_In_Pragma -- + ------------------------------------------- - function Mentions_Post_State (N : Node_Id) return Boolean; - -- Determine whether a subtree denoted by N mentions any construct that - -- denotes a post-state. + procedure Check_Result_And_Post_State_In_Pragma + (Prag : Node_Id; + Result_Seen : in out Boolean) + is + procedure Check_Expression (Expr : Node_Id); + -- Perform the 'Result and post-state checks on a given expression - procedure Check_Function_Result is - new Traverse_Proc (Is_Function_Result); + function Is_Function_Result (N : Node_Id) return Traverse_Result; + -- Attempt to find attribute 'Result in a subtree denoted by N - ---------------------- - -- Check_Expression -- - ---------------------- + function Is_Trivial_Boolean (N : Node_Id) return Boolean; + -- Determine whether source node N denotes "True" or "False" - procedure Check_Expression (Expr : Node_Id) is - begin - if not Is_Trivial_Boolean (Expr) then - Check_Function_Result (Expr); + function Mentions_Post_State (N : Node_Id) return Boolean; + -- Determine whether a subtree denoted by N mentions any construct + -- that denotes a post-state. - if not Mentions_Post_State (Expr) then - if Pragma_Name (Prag) = Name_Contract_Cases then - Error_Msg_N - ("contract case refers only to pre-state?T?", Expr); + procedure Check_Function_Result is + new Traverse_Proc (Is_Function_Result); - elsif Pragma_Name (Prag) = Name_Refined_Post then - Error_Msg_N - ("refined postcondition refers only to pre-state?T?", - Prag); + ---------------------- + -- Check_Expression -- + ---------------------- - else - Error_Msg_N - ("postcondition refers only to pre-state?T?", Prag); - end if; - end if; - end if; - end Check_Expression; + procedure Check_Expression (Expr : Node_Id) is + begin + if not Is_Trivial_Boolean (Expr) then + Check_Function_Result (Expr); - ------------------------ - -- Is_Function_Result -- - ------------------------ + if not Mentions_Post_State (Expr) then + if Pragma_Name (Prag) = Name_Contract_Cases then + Error_Msg_NE + ("contract case does not check the outcome of calling " + & "&?T?", Expr, Subp_Id); - function Is_Function_Result (N : Node_Id) return Traverse_Result is - begin - if Is_Attribute_Result (N) then - Result_Seen := True; - return Abandon; + elsif Pragma_Name (Prag) = Name_Refined_Post then + Error_Msg_NE + ("refined postcondition does not check the outcome of " + & "calling &?T?", Prag, Subp_Id); - -- Continue the traversal + else + Error_Msg_NE + ("postcondition does not check the outcome of calling " + & "&?T?", Prag, Subp_Id); + end if; + end if; + end if; + end Check_Expression; - else - return OK; - end if; - end Is_Function_Result; + ------------------------ + -- Is_Function_Result -- + ------------------------ - ------------------------ - -- Is_Trivial_Boolean -- - ------------------------ + function Is_Function_Result (N : Node_Id) return Traverse_Result is + begin + if Is_Attribute_Result (N) then + Result_Seen := True; + return Abandon; - function Is_Trivial_Boolean (N : Node_Id) return Boolean is - begin - return - Comes_From_Source (N) - and then Is_Entity_Name (N) - and then (Entity (N) = Standard_True - or else - Entity (N) = Standard_False); - end Is_Trivial_Boolean; + -- Continue the traversal - ------------------------- - -- Mentions_Post_State -- - ------------------------- + else + return OK; + end if; + end Is_Function_Result; - function Mentions_Post_State (N : Node_Id) return Boolean is - Post_State_Seen : Boolean := False; + ------------------------ + -- Is_Trivial_Boolean -- + ------------------------ - function Is_Post_State (N : Node_Id) return Traverse_Result; - -- Attempt to find a construct that denotes a post-state. If this is - -- the case, set flag Post_State_Seen. + function Is_Trivial_Boolean (N : Node_Id) return Boolean is + begin + return + Comes_From_Source (N) + and then Is_Entity_Name (N) + and then (Entity (N) = Standard_True + or else + Entity (N) = Standard_False); + end Is_Trivial_Boolean; - ------------------- - -- Is_Post_State -- - ------------------- + ------------------------- + -- Mentions_Post_State -- + ------------------------- - function Is_Post_State (N : Node_Id) return Traverse_Result is - Ent : Entity_Id; + function Mentions_Post_State (N : Node_Id) return Boolean is + Post_State_Seen : Boolean := False; - begin - if Nkind_In (N, N_Explicit_Dereference, N_Function_Call) then - Post_State_Seen := True; - return Abandon; + function Is_Post_State (N : Node_Id) return Traverse_Result; + -- Attempt to find a construct that denotes a post-state. If this + -- is the case, set flag Post_State_Seen. - elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then - Ent := Entity (N); + ------------------- + -- Is_Post_State -- + ------------------- - -- The entity may be modifiable through an implicit dereference + function Is_Post_State (N : Node_Id) return Traverse_Result is + Ent : Entity_Id; - if No (Ent) - or else Ekind (Ent) in Assignable_Kind - or else (Is_Access_Type (Etype (Ent)) - and then Nkind (Parent (N)) = N_Selected_Component) - then + begin + if Nkind_In (N, N_Explicit_Dereference, N_Function_Call) then Post_State_Seen := True; return Abandon; - end if; - elsif Nkind (N) = N_Attribute_Reference then - if Attribute_Name (N) = Name_Old then - return Skip; + elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then + Ent := Entity (N); - elsif Attribute_Name (N) = Name_Result then - Post_State_Seen := True; - return Abandon; + -- The entity may be modifiable through an implicit + -- dereference. + + if No (Ent) + or else Ekind (Ent) in Assignable_Kind + or else (Is_Access_Type (Etype (Ent)) + and then Nkind (Parent (N)) = + N_Selected_Component) + then + Post_State_Seen := True; + return Abandon; + end if; + + elsif Nkind (N) = N_Attribute_Reference then + if Attribute_Name (N) = Name_Old then + return Skip; + + elsif Attribute_Name (N) = Name_Result then + Post_State_Seen := True; + return Abandon; + end if; end if; - end if; - return OK; - end Is_Post_State; + return OK; + end Is_Post_State; - procedure Find_Post_State is new Traverse_Proc (Is_Post_State); + procedure Find_Post_State is new Traverse_Proc (Is_Post_State); - -- Start of processing for Mentions_Post_State + -- Start of processing for Mentions_Post_State + begin + Find_Post_State (N); + + return Post_State_Seen; + end Mentions_Post_State; + + -- Local variables + + Expr : constant Node_Id := + Get_Pragma_Arg + (First (Pragma_Argument_Associations (Prag))); + Nam : constant Name_Id := Pragma_Name (Prag); + CCase : Node_Id; + + -- Start of processing for Check_Result_And_Post_State_In_Pragma + begin - Find_Post_State (N); + -- Examine all consequences - return Post_State_Seen; - end Mentions_Post_State; + if Nam = Name_Contract_Cases then + CCase := First (Component_Associations (Expr)); + while Present (CCase) loop + Check_Expression (Expression (CCase)); + Next (CCase); + end loop; + + -- Examine the expression of a postcondition + + else pragma Assert (Nam_In (Nam, Name_Postcondition, + Name_Refined_Post)); + Check_Expression (Expr); + end if; + end Check_Result_And_Post_State_In_Pragma; + + -------------------------- + -- Has_In_Out_Parameter -- + -------------------------- + + function Has_In_Out_Parameter (Subp_Id : Entity_Id) return Boolean is + Formal : Entity_Id; + + begin + -- Traverse the formals looking for an IN OUT parameter + + Formal := First_Formal (Subp_Id); + while Present (Formal) loop + if Ekind (Formal) = E_In_Out_Parameter then + return True; + end if; + + Next_Formal (Formal); + end loop; + + return False; + end Has_In_Out_Parameter; + -- Local variables - Expr : constant Node_Id := - Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag))); - Nam : constant Name_Id := Pragma_Name (Prag); - CCase : Node_Id; + Items : constant Node_Id := Contract (Subp_Id); + Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Case_Prag : Node_Id := Empty; + Post_Prag : Node_Id := Empty; + Prag : Node_Id; + Seen_In_Case : Boolean := False; + Seen_In_Post : Boolean := False; + Spec_Id : Entity_Id; -- Start of processing for Check_Result_And_Post_State begin - -- Examine all consequences + -- The lack of attribute 'Result or a post-state is classified as a + -- suspicious contract. Do not perform the check if the corresponding + -- swich is not set. - if Nam = Name_Contract_Cases then - CCase := First (Component_Associations (Expr)); - while Present (CCase) loop - Check_Expression (Expression (CCase)); + if not Warn_On_Suspicious_Contract then + return; - Next (CCase); - end loop; + -- Nothing to do if there is no contract - -- Examine the expression of a postcondition + elsif No (Items) then + return; + end if; - else pragma Assert (Nam_In (Nam, Name_Postcondition, Name_Refined_Post)); - Check_Expression (Expr); + -- Retrieve the entity of the subprogram spec (if any) + + if Nkind (Subp_Decl) = N_Subprogram_Body + and then Present (Corresponding_Spec (Subp_Decl)) + then + Spec_Id := Corresponding_Spec (Subp_Decl); + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); + + else + Spec_Id := Subp_Id; end if; + + -- Examine all postconditions for attribute 'Result and a post-state + + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Nam_In (Pragma_Name (Prag), Name_Postcondition, + Name_Refined_Post) + and then not Error_Posted (Prag) + then + Post_Prag := Prag; + Check_Result_And_Post_State_In_Pragma (Prag, Seen_In_Post); + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Examine the contract cases of the subprogram for attribute 'Result + -- and a post-state. + + Prag := Contract_Test_Cases (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Contract_Cases + and then not Error_Posted (Prag) + then + Case_Prag := Prag; + Check_Result_And_Post_State_In_Pragma (Prag, Seen_In_Case); + end if; + + Prag := Next_Pragma (Prag); + end loop; + + -- Do not emit any errors if the subprogram is not a function + + if not Ekind_In (Spec_Id, E_Function, E_Generic_Function) then + null; + + -- Regardless of whether the function has postconditions or contract + -- cases, or whether they mention attribute 'Result, an IN OUT formal + -- parameter is always treated as a result. + + elsif Has_In_Out_Parameter (Spec_Id) then + null; + + -- The function has both a postcondition and contract cases and they do + -- not mention attribute 'Result. + + elsif Present (Case_Prag) + and then not Seen_In_Case + and then Present (Post_Prag) + and then not Seen_In_Post + then + Error_Msg_N + ("neither postcondition nor contract cases mention function " + & "result?T?", Post_Prag); + + -- The function has contract cases only and they do not mention + -- attribute 'Result. + + elsif Present (Case_Prag) and then not Seen_In_Case then + Error_Msg_N ("contract cases do not mention result?T?", Case_Prag); + + -- The function has postconditions only and they do not mention + -- attribute 'Result. + + elsif Present (Post_Prag) and then not Seen_In_Post then + Error_Msg_N + ("postcondition does not mention function result?T?", Post_Prag); + end if; end Check_Result_And_Post_State; ------------------------------ @@ -4336,6 +4468,27 @@ end if; end Corresponding_Generic_Type; + --------------------------- + -- Corresponding_Spec_Of -- + --------------------------- + + function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id is + begin + if Nkind (Subp_Decl) = N_Subprogram_Body + and then Present (Corresponding_Spec (Subp_Decl)) + then + return Corresponding_Spec (Subp_Decl); + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + return Corresponding_Spec_Of_Stub (Subp_Decl); + + else + return Defining_Entity (Subp_Decl); + end if; + end Corresponding_Spec_Of; + -------------------- -- Current_Entity -- -------------------- @@ -7009,32 +7162,6 @@ end if; end Get_Enum_Lit_From_Pos; - --------------------------------- - -- Get_Ensures_From_CTC_Pragma -- - --------------------------------- - - function Get_Ensures_From_CTC_Pragma (N : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (N); - Res : Node_Id; - - begin - if List_Length (Args) = 4 then - Res := Pick (Args, 4); - - elsif List_Length (Args) = 3 then - Res := Pick (Args, 3); - - if Chars (Res) /= Name_Ensures then - Res := Empty; - end if; - - else - Res := Empty; - end if; - - return Res; - end Get_Ensures_From_CTC_Pragma; - ------------------------ -- Get_Generic_Entity -- ------------------------ @@ -7294,29 +7421,6 @@ return R; end Get_Renamed_Entity; - ---------------------------------- - -- Get_Requires_From_CTC_Pragma -- - ---------------------------------- - - function Get_Requires_From_CTC_Pragma (N : Node_Id) return Node_Id is - Args : constant List_Id := Pragma_Argument_Associations (N); - Res : Node_Id; - - begin - if List_Length (Args) >= 3 then - Res := Pick (Args, 3); - - if Chars (Res) /= Name_Requires then - Res := Empty; - end if; - - else - Res := Empty; - end if; - - return Res; - end Get_Requires_From_CTC_Pragma; - ------------------------- -- Get_Subprogram_Body -- ------------------------- @@ -8804,6 +8908,41 @@ return Is_Floating_Point_Type (E) and then Signed_Zeros_On_Target; end Has_Signed_Zeros; + ------------------------------ + -- Has_Significant_Contract -- + ------------------------------ + + function Has_Significant_Contract (Subp_Id : Entity_Id) return Boolean is + Subp_Nam : constant Name_Id := Chars (Subp_Id); + + begin + -- _Finalizer procedure + + if Subp_Nam = Name_uFinalizer then + return False; + + -- _Postconditions procedure + + elsif Subp_Nam = Name_uPostconditions then + return False; + + -- Predicate function + + elsif Ekind (Subp_Id) = E_Function + and then Is_Predicate_Function (Subp_Id) + then + return False; + + -- TSS subprogram + + elsif Get_TSS_Name (Subp_Id) /= TSS_Null then + return False; + + else + return True; + end if; + end Has_Significant_Contract; + ----------------------------- -- Has_Static_Array_Bounds -- ----------------------------- @@ -9576,7 +9715,6 @@ if Is_Subprogram_Or_Generic_Subprogram (Subp) and then Is_Subprogram_Or_Generic_Subprogram (From_Subp) - and then Present (Contract (Subp)) and then Present (Contract (From_Subp)) then Inherit_Pragma (Pragma_Extensions_Visible); @@ -9696,6 +9834,23 @@ end Inspect_Deferred_Constant_Completion; ----------------------------- + -- Install_Generic_Formals -- + ----------------------------- + + procedure Install_Generic_Formals (Subp_Id : Entity_Id) is + E : Entity_Id; + + begin + pragma Assert (Is_Generic_Subprogram (Subp_Id)); + + E := First_Entity (Subp_Id); + while Present (E) loop + Install_Entity (E); + Next_Entity (E); + end loop; + end Install_Generic_Formals; + + ----------------------------- -- Is_Actual_Out_Parameter -- ----------------------------- @@ -15344,71 +15499,68 @@ end if; end Object_Access_Level; - -------------------------- - -- Original_Aspect_Name -- - -------------------------- + --------------------------------- + -- Original_Aspect_Pragma_Name -- + --------------------------------- - function Original_Aspect_Name (N : Node_Id) return Name_Id is - Pras : Node_Id; - Name : Name_Id; + function Original_Aspect_Pragma_Name (N : Node_Id) return Name_Id is + Item : Node_Id; + Item_Nam : Name_Id; begin pragma Assert (Nkind_In (N, N_Aspect_Specification, N_Pragma)); - Pras := N; - if Is_Rewrite_Substitution (Pras) - and then Nkind (Original_Node (Pras)) = N_Pragma - then - Pras := Original_Node (Pras); - end if; + Item := N; - -- Case where we came from aspect specication + -- The pragma was generated to emulate an aspect, use the original + -- aspect specification. - if Nkind (Pras) = N_Pragma and then From_Aspect_Specification (Pras) then - Pras := Corresponding_Aspect (Pras); + if Nkind (Item) = N_Pragma and then From_Aspect_Specification (Item) then + Item := Corresponding_Aspect (Item); end if; - -- Get name from aspect or pragma + -- Retrieve the name of the aspect/pragma. Note that Pre, Pre_Class, + -- Post and Post_Class rewrite their pragma identifier to preserve the + -- original name. + -- ??? this is kludgey - if Nkind (Pras) = N_Pragma then - Name := Pragma_Name (Pras); + if Nkind (Item) = N_Pragma then + Item_Nam := Chars (Original_Node (Pragma_Identifier (Item))); + else - Name := Chars (Identifier (Pras)); + pragma Assert (Nkind (Item) = N_Aspect_Specification); + Item_Nam := Chars (Identifier (Item)); end if; - -- Deal with 'Class + -- Deal with 'Class by converting the name to its _XXX form - if Class_Present (Pras) then - case Name is + if Class_Present (Item) then + if Item_Nam = Name_Invariant then + Item_Nam := Name_uInvariant; - -- Names that need converting to special _xxx form + elsif Nam_In (Item_Nam, Name_Post, Name_Post_Class) then + Item_Nam := Name_uPost; - when Name_Pre | - Name_Pre_Class => - Name := Name_uPre; + elsif Nam_In (Item_Nam, Name_Pre, Name_Pre_Class) then + Item_Nam := Name_uPre; - when Name_Post | - Name_Post_Class => - Name := Name_uPost; + elsif Item_Nam = Name_Invariant then + Item_Nam := Name_uInvariant; - when Name_Invariant => - Name := Name_uInvariant; + elsif Nam_In (Item_Nam, Name_Type_Invariant, + Name_Type_Invariant_Class) + then + Item_Nam := Name_uType_Invariant; - when Name_Type_Invariant | - Name_Type_Invariant_Class => - Name := Name_uType_Invariant; + -- Nothing to do for other cases (e.g. a Check that derived from + -- Pre_Class and has the flag set). Also we do nothing if the name + -- is already in special _xxx form. - -- Nothing to do for other cases (e.g. a Check that derived - -- from Pre_Class and has the flag set). Also we do nothing - -- if the name is already in special _xxx form. - - when others => - null; - end case; + end if; end if; - return Name; - end Original_Aspect_Name; + return Item_Nam; + end Original_Aspect_Pragma_Name; -------------------------------------- -- Original_Corresponding_Operation -- Index: sem_util.ads =================================================================== --- sem_util.ads (revision 221098) +++ sem_util.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -321,13 +321,10 @@ -- N is one of the statement forms that is a potentially blocking -- operation. If it appears within a protected action, emit warning. - procedure Check_Result_And_Post_State - (Prag : Node_Id; - Result_Seen : in out Boolean); - -- Determine whether pragma Prag mentions attribute 'Result and whether - -- the pragma contains an expression that evaluates differently in pre- - -- and post-state. Prag is a [refined] postcondition or a contract-cases - -- pragma. Result_Seen is set when the pragma mentions attribute 'Result. + procedure Check_Result_And_Post_State (Subp_Id : Entity_Id); + -- Determine whether the contract of subprogram Subp_Id mentions attribute + -- 'Result and it contains an expression that evaluates differently in pre- + -- and post-state. procedure Check_Unprotected_Access (Context : Node_Id; @@ -419,6 +416,11 @@ -- attribute, except in the case of formal private and derived types. -- Possible optimization??? + function Corresponding_Spec_Of (Subp_Decl : Node_Id) return Entity_Id; + -- Return the corresponding spec of Subp_Decl when it denotes a body [stub] + -- or the defining entity of subprogram declaration Subp_Decl in all other + -- cases. + function Current_Entity (N : Node_Id) return Entity_Id; pragma Inline (Current_Entity); -- Find the currently visible definition for a given identifier, that is to @@ -819,10 +821,6 @@ -- If expression N references a part of an object, return this object. -- Otherwise return Empty. Expression N should have been resolved already. - function Get_Ensures_From_CTC_Pragma (N : Node_Id) return Node_Id; - -- Return the Ensures component of Test_Case pragma N, or Empty otherwise - -- Bad name now that this no longer applies to Contract_Case ??? - function Get_Generic_Entity (N : Node_Id) return Entity_Id; -- Returns the true generic entity in an instantiation. If the name in the -- instantiation is a renaming, the function returns the renamed generic. @@ -899,10 +897,6 @@ -- not a renamed entity, returns its argument. It is an error to call this -- with any other kind of entity. - function Get_Requires_From_CTC_Pragma (N : Node_Id) return Node_Id; - -- Return the Requires component of Test_Case pragma N, or Empty otherwise - -- Bad name now that this no longer applies to Contract_Case ??? - function Get_Subprogram_Entity (Nod : Node_Id) return Entity_Id; -- Nod is either a procedure call statement, or a function call, or an -- accept statement node. This procedure finds the Entity_Id of the related @@ -1011,6 +1005,11 @@ -- Determines if the floating-point type E supports signed zeros. -- Returns False if E is not a floating-point type. + function Has_Significant_Contract (Subp_Id : Entity_Id) return Boolean; + -- Determine whether subprogram [body] Subp_Id has a significant contract. + -- All subprograms have a N_Contract node, but this does not mean that the + -- contract is useful. + function Has_Static_Array_Bounds (Typ : Node_Id) return Boolean; -- Return whether an array type has static bounds @@ -1128,6 +1127,10 @@ -- whether they have been completed by a full constant declaration or an -- Import pragma. Emit the error message if that is not the case. + procedure Install_Generic_Formals (Subp_Id : Entity_Id); + -- Install both the generic formal parameters and the formal parameters of + -- generic subprogram Subp_Id into visibility. + function Is_Actual_Out_Parameter (N : Node_Id) return Boolean; -- Determines if N is an actual parameter of out mode in a subprogram call @@ -1673,15 +1676,19 @@ -- corresponding operation of S is the original corresponding operation of -- S2. Otherwise, it is S itself. - function Original_Aspect_Name (N : Node_Id) return Name_Id; - -- N is a pragma node or aspect specification node. This function returns - -- the name of the pragma or aspect in original source form, taking into - -- account possible rewrites, and also cases where a pragma comes from an - -- aspect (in such cases, the name can be different from the pragma name, - -- e.g. a Pre aspect generates a Precondition pragma). This also deals with - -- the presence of 'Class, which results in one of the special names - -- Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being - -- returned to represent the corresponding aspects with x'Class names. + function Original_Aspect_Pragma_Name (N : Node_Id) return Name_Id; + -- Retrieve the name of aspect or pragma N taking into account a possible + -- rewrite and whether the pragma is generated from an aspect as the names + -- may be different. The routine also deals with 'Class in which case it + -- returns the following values: + -- + -- Invariant -> Name_uInvariant + -- Post -> Name_uPost + -- Post'Class -> Name_uPost + -- Pre -> Name_uPre + -- Pre'Class -> Name_uPre + -- Type_Invariant -> Name_uType_Invariant + -- Type_Invariant'Class -> Name_uType_Invariant function Policy_In_Effect (Policy : Name_Id) return Name_Id; -- Given a policy, return the policy identifier associated with it. If no Index: sem_attr.adb =================================================================== --- sem_attr.adb (revision 221098) +++ sem_attr.adb (working copy) @@ -59,6 +59,7 @@ with Sem_Elab; use Sem_Elab; with Sem_Elim; use Sem_Elim; with Sem_Eval; use Sem_Eval; +with Sem_Prag; use Sem_Prag; with Sem_Res; use Sem_Res; with Sem_Type; use Sem_Type; with Sem_Util; use Sem_Util; @@ -4561,7 +4562,7 @@ ---------------------------- procedure Check_Use_In_Test_Case (Prag : Node_Id) is - Ensures : constant Node_Id := Get_Ensures_From_CTC_Pragma (Prag); + Ensures : constant Node_Id := Test_Case_Arg (Prag, Name_Ensures); Expr : Node_Id; begin @@ -4984,269 +4985,373 @@ ------------ when Attribute_Result => Result : declare - Post_Id : Entity_Id; - -- The entity of the _Postconditions procedure + procedure Check_Placement_In_Check (Prag : Node_Id); + -- Verify that attribute 'Result appears within pragma Check that + -- emulates a postcondition. - Prag : Node_Id; - -- During pre-analysis, Prag is the enclosing pragma node if any + procedure Check_Placement_In_Contract_Cases (Prag : Node_Id); + -- Verify that attribute 'Result appears within a consequence of + -- pragma Contract_Cases. - Subp_Id : Entity_Id; - -- The entity of the enclosing subprogram + procedure Check_Placement_In_Test_Case (Prag : Node_Id); + -- Verify that attribute 'Result appears within the Ensures argument + -- of pragma Test_Case. - begin - -- Find the proper enclosing scope + function Is_Within + (Nod : Node_Id; + Encl_Nod : Node_Id) return Boolean; + -- Subsidiary to Check_Placemenet_In_XXX_Case. Determine whether + -- arbitrary node Nod is within enclosing node Encl_Nod. - Post_Id := Current_Scope; - while Present (Post_Id) loop + ------------------------------ + -- Check_Placement_In_Check -- + ------------------------------ - -- Skip generated loops + procedure Check_Placement_In_Check (Prag : Node_Id) is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + Nam : constant Name_Id := Chars (Get_Pragma_Arg (First (Args))); - if Ekind (Post_Id) = E_Loop then - Post_Id := Scope (Post_Id); + begin + -- The "Name" argument of pragma Check denotes a postcondition - -- Skip the special _Parent scope generated to capture references - -- to formals during the process of subprogram inlining. - - elsif Ekind (Post_Id) = E_Function - and then Chars (Post_Id) = Name_uParent + if Nam_In (Nam, Name_Post, + Name_Postcondition, + Name_Refined_Post) then - Post_Id := Scope (Post_Id); + null; - -- Otherwise this must be _Postconditions + -- Otherwise the placement of attribute 'Result is illegal else - exit; + Error_Attr + ("% attribute can only appear in postcondition of function", + P); end if; - end loop; + end Check_Placement_In_Check; - Subp_Id := Scope (Post_Id); + --------------------------------------- + -- Check_Placement_In_Contract_Cases -- + --------------------------------------- - -- If the enclosing subprogram is always inlined, the enclosing - -- postcondition will not be propagated to the expanded call. + procedure Check_Placement_In_Contract_Cases (Prag : Node_Id) is + Args : constant List_Id := Pragma_Argument_Associations (Prag); + Cases : constant Node_Id := Get_Pragma_Arg (First (Args)); + CCase : Node_Id; - if not In_Spec_Expression - and then Has_Pragma_Inline_Always (Subp_Id) - and then Warn_On_Redundant_Constructs - then - Error_Msg_N - ("postconditions on inlined functions not enforced?r?", N); - end if; + begin + if Present (Component_Associations (Cases)) then + CCase := First (Component_Associations (Cases)); + while Present (CCase) loop - -- If we are in the scope of a function and in Spec_Expression mode, - -- this is likely the prescan of the postcondition (or contract case, - -- or test case) pragma, and we just set the proper type. If there is - -- an error it will be caught when the real Analyze call is done. + -- Guard against a malformed contract case. Detect whether + -- attribute 'Result appears within the consequence of the + -- current contract case. - if Ekind (Post_Id) = E_Function and then In_Spec_Expression then + if Nkind (CCase) = N_Component_Association + and then Is_Within (N, Expression (CCase)) + then + return; + end if; - -- Check OK prefix + Next (CCase); + end loop; + end if; - if Chars (Post_Id) /= Chars (P) then - Error_Msg_Name_1 := Name_Result; - Error_Msg_NE - ("incorrect prefix for % attribute, expected &", P, Post_Id); - Error_Attr; + -- Otherwise pragma Contract_Cases is either malformed in some + -- way or attribute 'Result does not appear within a consequence + -- expression. + + Error_Attr ("% attribute misplaced inside contract cases", P); + end Check_Placement_In_Contract_Cases; + + ---------------------------------- + -- Check_Placement_In_Test_Case -- + ---------------------------------- + + procedure Check_Placement_In_Test_Case (Prag : Node_Id) is + begin + -- Detect whether attribute 'Result appears within the "Ensures" + -- expression of pragma Test_Case. + + if not Is_Within (N, Test_Case_Arg (Prag, Name_Ensures)) then + Error_Attr ("% attribute misplaced inside test case", P); end if; + end Check_Placement_In_Test_Case; - -- Check in postcondition, Test_Case or Contract_Cases of function + --------------- + -- Is_Within -- + --------------- - Prag := N; - while Present (Prag) - and then not Nkind_In (Prag, N_Pragma, - N_Function_Specification, - N_Aspect_Specification, - N_Subprogram_Body) - loop - Prag := Parent (Prag); - end loop; + function Is_Within + (Nod : Node_Id; + Encl_Nod : Node_Id) return Boolean + is + Par : Node_Id; - -- In ASIS mode, the aspect itself is analyzed, in addition to the - -- corresponding pragma. Do not issue errors when analyzing the - -- aspect. + begin + Par := Nod; + while Present (Par) loop + if Par = Encl_Nod then + return True; - if Nkind (Prag) = N_Aspect_Specification then - null; + -- Prevent the search from going too far - -- Must have a pragma + elsif Is_Body_Or_Package_Declaration (Par) then + exit; + end if; - elsif Nkind (Prag) /= N_Pragma then - Error_Attr - ("% attribute can only appear in postcondition of function", - P); + Par := Parent (Par); + end loop; - -- Processing depends on which pragma we have + return False; + end Is_Within; - else - case Get_Pragma_Id (Prag) is - when Pragma_Test_Case => - declare - Arg_Ens : constant Node_Id := - Get_Ensures_From_CTC_Pragma (Prag); - Arg : Node_Id; + -- Local variables - begin - Arg := N; - while Arg /= Prag and then Arg /= Arg_Ens loop - Arg := Parent (Arg); - end loop; + In_Post : Boolean := False; + Prag : Node_Id; + Prag_Id : Pragma_Id; + Pref_Id : Entity_Id; + Spec_Id : Entity_Id; + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; + Subp_Spec : Node_Id; - if Arg /= Arg_Ens then - Error_Attr - ("% attribute misplaced inside test case", P); - end if; - end; + -- Start of processing for Result - when Pragma_Contract_Cases => - declare - Aggr : constant Node_Id := - Expression (First - (Pragma_Argument_Associations (Prag))); - Arg : Node_Id; + begin + -- The attribute reference is a primary. If any expressions follow, + -- then the attribute reference is an indexable object. Transform the + -- attribute into an indexed component and analyze it. - begin - Arg := N; - while Arg /= Prag - and then Parent (Parent (Arg)) /= Aggr - loop - Arg := Parent (Arg); - end loop; + if Present (E1) then + Rewrite (N, + Make_Indexed_Component (Loc, + Prefix => + Make_Attribute_Reference (Loc, + Prefix => Relocate_Node (P), + Attribute_Name => Name_Result), + Expressions => Expressions (N))); + Analyze (N); + return; + end if; - -- At this point, Parent (Arg) should be a component - -- association. Attribute Result is only allowed in - -- the expression part of this association. + -- Traverse the parent chain to find the aspect or pragma where + -- attribute 'Result resides. - if Nkind (Parent (Arg)) /= N_Component_Association - or else Arg /= Expression (Parent (Arg)) - then - Error_Attr - ("% attribute misplaced inside contract cases", - P); - end if; - end; + Prag := N; + while Present (Prag) loop + if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then + exit; - when Pragma_Postcondition | Pragma_Refined_Post => - null; + -- Prevent the search from going too far - when others => - Error_Attr - ("% attribute can only appear in postcondition " - & "of function", P); - end case; + elsif Is_Body_Or_Package_Declaration (Prag) then + exit; end if; - -- The attribute reference is a primary. If expressions follow, - -- the attribute reference is really an indexable object, so - -- rewrite and analyze as an indexed component. + Prag := Parent (Prag); + end loop; - if Present (E1) then - Rewrite (N, - Make_Indexed_Component (Loc, - Prefix => - Make_Attribute_Reference (Loc, - Prefix => Relocate_Node (Prefix (N)), - Attribute_Name => Name_Result), - Expressions => Expressions (N))); - Analyze (N); + -- Do not emit an error when preanalyzing an aspect for ASIS. If the + -- placement of attribute 'Result is illegal, the error is reported + -- when analyzing the corresponding pragma. + + if ASIS_Mode and then Nkind (Prag) = N_Aspect_Specification then + null; + + -- Attribute 'Result is allowed to appear only in postcondition-like + -- pragmas. + + elsif Nkind (Prag) = N_Pragma then + Prag_Id := Get_Pragma_Id (Prag); + + if Prag_Id = Pragma_Check then + Check_Placement_In_Check (Prag); + + elsif Prag_Id = Pragma_Contract_Cases then + Check_Placement_In_Contract_Cases (Prag); + + elsif Prag_Id = Pragma_Postcondition + or else Prag_Id = Pragma_Refined_Post + then + null; + + elsif Prag_Id = Pragma_Test_Case then + Check_Placement_In_Test_Case (Prag); + + else + Error_Attr + ("% attribute can only appear in postcondition of function", + P); return; end if; - Set_Etype (N, Etype (Post_Id)); + -- Otherwise the placement of the attribute is illegal - -- If several functions with that name are visible, the intended - -- one is the current scope. + else + Error_Attr + ("% attribute can only appear in postcondition of function", P); + return; + end if; - if Is_Overloaded (P) then - Set_Entity (P, Post_Id); - Set_Is_Overloaded (P, False); - end if; + -- Attribute 'Result appears within a postcondition-like pragma. Find + -- the related subprogram subject to the pragma. - -- Check the legality of attribute 'Result when it appears inside - -- pragma Refined_Post. These specialized checks are required only - -- when code generation is disabled. In the general case pragma - -- Refined_Post is transformed into pragma Check by Process_PPCs - -- which in turn is relocated to procedure _Postconditions. From - -- then on the legality of 'Result is determined as usual. + if Nkind (Prag) = N_Aspect_Specification then + Subp_Decl := Parent (Prag); + else + Subp_Decl := Find_Related_Subprogram_Or_Body (Prag); + end if; - elsif not Expander_Active and then In_Refined_Post then + -- The pragma where attribute 'Result appears is associated with a + -- subprogram declaration or a body. - -- Routine _Postconditions has not been generated yet, the nearest - -- enclosing subprogram is denoted by the current scope. + if Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration, + N_Entry_Declaration, + N_Generic_Subprogram_Declaration, + N_Subprogram_Body, + N_Subprogram_Body_Stub, + N_Subprogram_Declaration) + then + Subp_Id := Defining_Entity (Subp_Decl); - if Ekind (Post_Id) /= E_Procedure - or else Chars (Post_Id) /= Name_uPostconditions - then - Subp_Id := Current_Scope; + -- Attribute 'Result is part of the _Postconditions procedure of + -- the related subprogram. Retrieve the related subprogram. + + if Chars (Subp_Id) = Name_uPostconditions then + In_Post := True; + Subp_Decl := Parent (Subp_Decl); + Subp_Id := Scope (Subp_Id); end if; - -- The prefix denotes the nearest enclosing function + -- Retrieve the entity of the spec (if any) - if Is_Entity_Name (P) - and then Ekind (Entity (P)) = E_Function - and then Entity (P) = Subp_Id + if Nkind (Subp_Decl) = N_Subprogram_Body + and then Present (Corresponding_Spec (Subp_Decl)) then - null; + Spec_Id := Corresponding_Spec (Subp_Decl); - -- Otherwise the use of 'Result is illegal + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then Present (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl); else - Error_Msg_Name_2 := Chars (Subp_Id); - Error_Attr ("incorrect prefix for % attribute, expected %", P); + Spec_Id := Subp_Id; end if; - Set_Etype (N, Etype (Subp_Id)); + -- When the subprogram is always inlined, the postcondition will + -- not be propagated to the expanded body. - -- Body case, where we must be inside a generated _Postconditions - -- procedure, and the prefix must be on the scope stack, or else the - -- attribute use is definitely misplaced. The postcondition itself - -- may have generated transient scopes, and is not necessarily the - -- current one. + if Warn_On_Redundant_Constructs + and then Has_Pragma_Inline_Always (Spec_Id) + then + Error_Msg_N + ("postconditions on inlined functions not enforced?r?", P); + end if; - else - while Present (Post_Id) - and then Post_Id /= Standard_Standard - loop - if Chars (Post_Id) = Name_uPostconditions then - exit; - else - Post_Id := Scope (Post_Id); + -- Ensure that the prefix of attribute 'Result denotes the related + -- subprogram. + + if Is_Entity_Name (P) then + Pref_Id := Entity (P); + + -- When a subprogram with contract assertions is imported, it + -- is encapsulated in a wrapper. In this case the scope of the + -- wrapper denotes the original imported subprogram. + + if Is_Imported (Pref_Id) then + Pref_Id := Scope (Pref_Id); end if; - end loop; - Subp_Id := Scope (Post_Id); + if Ekind_In (Pref_Id, E_Function, E_Generic_Function) then - if Chars (Post_Id) = Name_uPostconditions - and then Ekind (Subp_Id) = E_Function - then - -- Check OK prefix + -- The prefix of attribute 'Result denotes the entity of + -- some other unrelated function. - if Nkind_In (P, N_Identifier, N_Operator_Symbol) - and then Chars (P) = Chars (Subp_Id) - then - null; + if Pref_Id /= Spec_Id then + Subp_Spec := Parent (Spec_Id); - -- Within an instance, the prefix designates the local renaming - -- of the original generic. + -- Attribute 'Result appears in a postcondition of a + -- generic function that acts as a compilation unit: - elsif Is_Entity_Name (P) - and then Ekind (Entity (P)) = E_Function - and then Present (Alias (Entity (P))) - and then Chars (Alias (Entity (P))) = Chars (Subp_Id) - then - null; + -- generic + -- function Gen_Func return ... + -- with Post => Gen_Func'Result ...; + -- When the function is instantiated, the Chars field of + -- attribute 'Result's prefix still denotes the generic + -- function. Note that any preemptive transformation is + -- impossible without a proper analysis. The structure of + -- the anonymous wrapper package is as follows: + + -- package Anon_Gen_Pack is + -- + -- function Subp_Decl return ...; + -- pragma Postcondition (Gen_Func'Result ...); + -- function Gen_Func ... renames Subp_Decl; + -- end Anon_Gen_Pack; + + -- Recognize this case and do not flag it as illegal + + if Nkind (Subp_Spec) = N_Function_Specification + and then Present (Generic_Parent (Subp_Spec)) + then + if Generic_Parent (Subp_Spec) = Pref_Id then + null; + + elsif Ekind (Pref_Id) = E_Function + and then Present (Alias (Pref_Id)) + and then Alias (Pref_Id) = Spec_Id + then + null; + + else + Error_Msg_Name_2 := Chars (Spec_Id); + Error_Attr + ("incorrect prefix for % attribute, expected %", + P); + end if; + + -- Otherwise the context is not a function instantiation + -- and the prefix is illegal + + else + Error_Msg_Name_2 := Chars (Spec_Id); + Error_Attr + ("incorrect prefix for % attribute, expected %", P); + end if; + end if; + + -- Otherwise the attribute's prefix denotes some other form of + -- a non-function subprogram. + else - Error_Msg_Name_2 := Chars (Subp_Id); Error_Attr - ("incorrect prefix for % attribute, expected %", P); + ("% attribute can only appear in postcondition of " + & "function", P); end if; - Rewrite (N, Make_Identifier (Sloc (N), Name_uResult)); + -- Otherwise the prefix is illegal + + else + Error_Msg_Name_2 := Chars (Spec_Id); + Error_Attr ("incorrect prefix for % attribute, expected %", P); + end if; + + -- Attribute 'Result is part of the _Postconditions procedure of + -- the related subprogram. Rewrite the attribute as a reference to + -- the _Result formal parameter of _Postconditions. + + if In_Post then + Rewrite (N, Make_Identifier (Loc, Name_uResult)); Analyze_And_Resolve (N, Etype (Subp_Id)); + -- Otherwise decorate the attribute + else - Error_Attr - ("% attribute can only appear in postcondition of function", - P); + Set_Etype (N, Etype (Subp_Id)); end if; end if; end Result; Index: exp_ch6.adb =================================================================== --- exp_ch6.adb (revision 221098) +++ exp_ch6.adb (working copy) @@ -202,10 +202,9 @@ -- secondary stack using 'reference. procedure Expand_Non_Function_Return (N : Node_Id); - -- Called by Expand_N_Simple_Return_Statement in case we're returning from - -- a procedure body, entry body, accept statement, or extended return - -- statement. Note that all non-function returns are simple return - -- statements. + -- Expand a simple return statement found in a procedure body, entry body, + -- accept statement, or an extended return statement. Note that all non- + -- function returns are simple return statements. function Expand_Protected_Object_Reference (N : Node_Id; @@ -4983,21 +4982,22 @@ ---------------- procedure Add_Return (S : List_Id) is - Last_Stm : Node_Id; - Loc : Source_Ptr; + Last_Stmt : Node_Id; + Loc : Source_Ptr; + Stmt : Node_Id; begin -- Get last statement, ignoring any Pop_xxx_Label nodes, which are -- not relevant in this context since they are not executable. - Last_Stm := Last (S); - while Nkind (Last_Stm) in N_Pop_xxx_Label loop - Prev (Last_Stm); + Last_Stmt := Last (S); + while Nkind (Last_Stmt) in N_Pop_xxx_Label loop + Prev (Last_Stmt); end loop; -- Now insert return unless last statement is a transfer - if not Is_Transfer (Last_Stm) then + if not Is_Transfer (Last_Stmt) then -- The source location for the return is the end label of the -- procedure if present. Otherwise use the sloc of the last @@ -5009,49 +5009,43 @@ if Nkind (Parent (S)) = N_Exception_Handler and then not Comes_From_Source (Parent (S)) then - Loc := Sloc (Last_Stm); + Loc := Sloc (Last_Stmt); elsif Present (End_Label (H)) then Loc := Sloc (End_Label (H)); else - Loc := Sloc (Last_Stm); + Loc := Sloc (Last_Stmt); end if; - declare - Rtn : constant Node_Id := Make_Simple_Return_Statement (Loc); + -- Append return statement, and set analyzed manually. We can't + -- call Analyze on this return since the scope is wrong. - begin - -- Append return statement, and set analyzed manually. We can't - -- call Analyze on this return since the scope is wrong. + -- Note: it almost works to push the scope and then do the Analyze + -- call, but something goes wrong in some weird cases and it is + -- not worth worrying about ??? - -- Note: it almost works to push the scope and then do the - -- Analyze call, but something goes wrong in some weird cases - -- and it is not worth worrying about ??? + Stmt := Make_Simple_Return_Statement (Loc); - -- The return statement is handled properly, and the call - -- to the postcondition, inserted below, does not require - -- information from the body either. However, that call is - -- analyzed in the enclosing scope, and an elaboration check - -- might improperly be added to it. A guard in Sem_Elab is - -- needed to prevent that spurious check, see Check_Elab_Call. + -- The return statement is handled properly, and the call to the + -- postcondition, inserted below, does not require information + -- from the body either. However, that call is analyzed in the + -- enclosing scope, and an elaboration check might improperly be + -- added to it. A guard in Sem_Elab is needed to prevent that + -- spurious check, see Check_Elab_Call. - Append_To (S, Rtn); - Set_Analyzed (Rtn); + Append_To (S, Stmt); + Set_Analyzed (Stmt); - -- Call _Postconditions procedure if appropriate. We need to - -- do this explicitly because we did not analyze the generated - -- return statement above, so the call did not get inserted. + -- Call the _Postconditions procedure if the related subprogram + -- has contract assertions that need to be verified on exit. - if Ekind (Spec_Id) = E_Procedure - and then Has_Postconditions (Spec_Id) - then - pragma Assert (Present (Postcondition_Proc (Spec_Id))); - Insert_Action (Rtn, - Make_Procedure_Call_Statement (Loc, - Name => - New_Occurrence_Of - (Postcondition_Proc (Spec_Id), Loc))); - end if; - end; + if Ekind (Spec_Id) = E_Procedure + and then Present (Postconditions_Proc (Spec_Id)) + then + Insert_Action (Stmt, + Make_Procedure_Call_Statement (Loc, + Name => + New_Occurrence_Of (Postconditions_Proc (Spec_Id), Loc))); + end if; end if; end Add_Return; @@ -5206,7 +5200,8 @@ -- the initial value itself (which may well be invalid). -- Predicate checks are disabled as well (RM 6.4.1 (13/3)) - A := Make_Assignment_Statement (Loc, + A := + Make_Assignment_Statement (Loc, Name => New_Occurrence_Of (F, Loc), Expression => Get_Simple_Init_Val (Etype (F), N)); Set_Suppress_Assignment_Checks (A); @@ -5487,31 +5482,24 @@ procedure Expand_Non_Function_Return (N : Node_Id) is pragma Assert (No (Expression (N))); - Loc : constant Source_Ptr := Sloc (N); - Scope_Id : Entity_Id := - Return_Applies_To (Return_Statement_Entity (N)); - Kind : constant Entity_Kind := Ekind (Scope_Id); - Call : Node_Id; - Acc_Stat : Node_Id; - Goto_Stat : Node_Id; - Lab_Node : Node_Id; + Loc : constant Source_Ptr := Sloc (N); + Scope_Id : Entity_Id := Return_Applies_To (Return_Statement_Entity (N)); + Kind : constant Entity_Kind := Ekind (Scope_Id); + Call : Node_Id; + Acc_Stat : Node_Id; + Goto_Stat : Node_Id; + Lab_Node : Node_Id; begin - -- Call _Postconditions procedure if procedure with active - -- postconditions. Here, we use the Postcondition_Proc attribute, - -- which is needed for implicitly-generated returns. Functions - -- never have implicitly-generated returns, and there's no - -- room for Postcondition_Proc in E_Function, so we look up the - -- identifier Name_uPostconditions for function returns (see - -- Expand_Simple_Function_Return). + -- Call the _Postconditions procedure if the related subprogram has + -- contract assertions that need to be verified on exit. - if Ekind (Scope_Id) = E_Procedure - and then Has_Postconditions (Scope_Id) + if Ekind_In (Scope_Id, E_Entry, E_Entry_Family, E_Procedure) + and then Present (Postconditions_Proc (Scope_Id)) then - pragma Assert (Present (Postcondition_Proc (Scope_Id))); Insert_Action (N, Make_Procedure_Call_Statement (Loc, - Name => New_Occurrence_Of (Postcondition_Proc (Scope_Id), Loc))); + Name => New_Occurrence_Of (Postconditions_Proc (Scope_Id), Loc))); end if; -- If it is a return from a procedure do no extra steps @@ -6558,10 +6546,11 @@ end; end if; - -- Generate call to postcondition checks if they are present + -- Call the _Postconditions procedure if the related function has + -- contract assertions that need to be verified on exit. if Ekind (Scope_Id) = E_Function - and then Has_Postconditions (Scope_Id) + and then Present (Postconditions_Proc (Scope_Id)) then -- We are going to reference the returned value twice in this case, -- once in the call to _Postconditions, and once in the actual return @@ -6669,11 +6658,12 @@ end; end if; - -- Generate call to _postconditions + -- Generate call to _Postconditions Insert_Action (Exp, Make_Procedure_Call_Statement (Loc, - Name => Make_Identifier (Loc, Name_uPostconditions), + Name => + New_Occurrence_Of (Postconditions_Proc (Scope_Id), Loc), Parameter_Associations => New_List (Duplicate_Subexpr (Exp)))); end if; @@ -6697,11 +6687,10 @@ -- Expand_Subprogram_Contract -- -------------------------------- - procedure Expand_Subprogram_Contract - (N : Node_Id; - Spec_Id : Entity_Id; - Body_Id : Entity_Id) - is + procedure Expand_Subprogram_Contract (N : Node_Id) is + Body_Id : constant Entity_Id := Defining_Entity (N); + Spec_Id : constant Entity_Id := Corresponding_Spec (N); + procedure Add_Invariant_And_Predicate_Checks (Subp_Id : Entity_Id; Stmts : in out List_Id; @@ -6735,30 +6724,18 @@ -- the routine corrects the references of all formals of Inher_Id to -- point to the formals of Subp_Id. - procedure Collect_Body_Postconditions (Stmts : in out List_Id); - -- Process all postconditions found in the declarations of the body. The - -- routine appends the pragma Check equivalents to list Stmts. + procedure Process_Contract_Cases (Stmts : in out List_Id); + -- Process pragma Contract_Cases. This routine prepends items to the + -- body declarations and appends items to list Stmts. - procedure Collect_Spec_Postconditions - (Subp_Id : Entity_Id; - Stmts : in out List_Id); - -- Process all [inherited] postconditions of subprogram spec Subp_Id. - -- The routine appends the pragma Check equivalents to list Stmts. + procedure Process_Postconditions (Stmts : in out List_Id); + -- Collect all [inherited] spec and body postconditions and accumulate + -- their pragma Check equivalents in list Stmts. - procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id); - -- Process all [inherited] preconditions of subprogram spec Subp_Id. The - -- routine prepends the pragma Check equivalents to the declarations of - -- the body. + procedure Process_Preconditions; + -- Collect all [inherited] spec and body preconditions and prepend their + -- pragma Check equivalents to the declarations of the body. - procedure Prepend_To_Declarations (Item : Node_Id); - -- Prepend a single item to the declarations of the subprogram body - - procedure Process_Contract_Cases - (Subp_Id : Entity_Id; - Stmts : in out List_Id); - -- Process pragma Contract_Cases of subprogram spec Subp_Id. The routine - -- appends the expanded code to list Stmts. - ---------------------------------------- -- Add_Invariant_And_Predicate_Checks -- ---------------------------------------- @@ -6954,15 +6931,9 @@ begin Result := Empty; - -- Do not generate any checks if no code is being generated - - if not Expander_Active then - return; - end if; - -- Process the result of a function - if Ekind_In (Subp_Id, E_Function, E_Generic_Function) then + if Ekind (Subp_Id) = E_Function then Typ := Etype (Subp_Id); -- Generate _Result which is used in procedure _Postconditions to @@ -7103,25 +7074,23 @@ -- Local variables - Loc : constant Source_Ptr := Sloc (N); - Params : List_Id := No_List; - Proc_Id : Entity_Id; + Loc : constant Source_Ptr := Sloc (N); + Params : List_Id := No_List; + Proc_Bod : Node_Id; + Proc_Id : Entity_Id; -- Start of processing for Build_Postconditions_Procedure begin - -- Do not create the routine if no code is being generated - - if not Expander_Active then - return; - -- Nothing to do if there are no actions to check on exit - elsif No (Stmts) then + if No (Stmts) then return; end if; Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions); + Set_Debug_Info_Needed (Proc_Id); + Set_Postconditions_Proc (Subp_Id, Proc_Id); -- The related subprogram is a function, create the specification of -- parameter _Result. @@ -7152,13 +7121,12 @@ -- order reference. The body of _Postconditions must be placed after -- the declaration of Temp to preserve correct visibility. - -- Note that we set an explicit End_Label in order to override the - -- sloc of the implicit RETURN statement, and prevent it from - -- inheriting the sloc of one of the postconditions: this would cause - -- confusing debug info to be produced, interfering with coverage - -- analysis tools. + -- Set an explicit End_Lavel to override the sloc of the implicit + -- RETURN statement, and prevent it from inheriting the sloc of one + -- the postconditions: this would cause confusing debug into to be + -- produced, interfering with coverage analysis tools. - Insert_Before_First_Source_Declaration ( + Proc_Bod := Make_Subprogram_Body (Loc, Specification => Make_Procedure_Specification (Loc, @@ -7169,16 +7137,10 @@ Handled_Statement_Sequence => Make_Handled_Sequence_Of_Statements (Loc, Statements => Stmts, - End_Label => Make_Identifier (Loc, Chars (Proc_Id))))); + End_Label => Make_Identifier (Loc, Chars (Proc_Id)))); - -- Set the attributes of the related subprogram to capture the - -- generated procedure. - - if Ekind_In (Subp_Id, E_Generic_Procedure, E_Procedure) then - Set_Postcondition_Proc (Subp_Id, Proc_Id); - end if; - - Set_Has_Postconditions (Subp_Id); + Insert_Before_First_Source_Declaration (Proc_Bod); + Analyze (Proc_Bod); end Build_Postconditions_Procedure; ----------------------------------- @@ -7238,14 +7200,6 @@ Set_Comes_From_Source (Check_Prag, False); Set_Analyzed (Check_Prag, False); - -- For a postcondition pragma within a generic, preserve the pragma - -- for later expansion. This is also used when an error was detected, - -- thus setting Expander_Active to False. - - if Prag_Nam = Name_Postcondition and then not Expander_Active then - return Check_Prag; - end if; - if Present (Corresponding_Aspect (Prag)) then Nam := Chars (Identifier (Corresponding_Aspect (Prag))); else @@ -7282,61 +7236,105 @@ return Check_Prag; end Build_Pragma_Check_Equivalent; - --------------------------------- - -- Collect_Body_Postconditions -- - --------------------------------- + ---------------------------- + -- Process_Contract_Cases -- + ---------------------------- - procedure Collect_Body_Postconditions (Stmts : in out List_Id) is - procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id); - -- Process all postconditions of the kind denoted by Post_Nam + procedure Process_Contract_Cases (Stmts : in out List_Id) is + procedure Process_Contract_Cases_For (Subp_Id : Entity_Id); + -- Process pragma Contract_Cases for subprogram Subp_Id - ----------------------------------------- - -- Collect_Body_Postconditions_Of_Kind -- - ----------------------------------------- + -------------------------------- + -- Process_Contract_Cases_For -- + -------------------------------- - procedure Collect_Body_Postconditions_Of_Kind (Post_Nam : Name_Id) is - procedure Collect_Body_Postconditions_In_Decls - (First_Decl : Node_Id); - -- Process all postconditions found in a declarative list starting - -- with declaration First_Decl. + procedure Process_Contract_Cases_For (Subp_Id : Entity_Id) is + Items : constant Node_Id := Contract (Subp_Id); + Prag : Node_Id; - ------------------------------------------ - -- Collect_Body_Postconditions_In_Decls -- - ------------------------------------------ + begin + if Present (Items) then + Prag := Contract_Test_Cases (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Contract_Cases then + Expand_Contract_Cases + (CCs => Prag, + Subp_Id => Subp_Id, + Decls => Declarations (N), + Stmts => Stmts); + end if; - procedure Collect_Body_Postconditions_In_Decls - (First_Decl : Node_Id) - is - Check_Prag : Node_Id; - Decl : Node_Id; + Prag := Next_Pragma (Prag); + end loop; + end if; + end Process_Contract_Cases_For; - begin - -- Inspect the declarative list looking for a pragma that - -- matches the desired name. + -- Start of processing for Process_Contract_Cases - Decl := First_Decl; + begin + Process_Contract_Cases_For (Body_Id); + + if Present (Spec_Id) then + Process_Contract_Cases_For (Spec_Id); + end if; + end Process_Contract_Cases; + + ---------------------------- + -- Process_Postconditions -- + ---------------------------- + + procedure Process_Postconditions (Stmts : in out List_Id) is + procedure Process_Body_Postconditions (Post_Nam : Name_Id); + -- Collect all [refined] postconditions of a specific kind denoted + -- by Post_Nam that belong to the body and generate pragma Check + -- equivalents in list Stmts. + + procedure Process_Spec_Postconditions; + -- Collect all [inherited] postconditions of the spec and generate + -- pragma Check equivalents in list Stmts. + + --------------------------------- + -- Process_Body_Postconditions -- + --------------------------------- + + procedure Process_Body_Postconditions (Post_Nam : Name_Id) is + Items : constant Node_Id := Contract (Body_Id); + Unit_Decl : constant Node_Id := Parent (N); + Decl : Node_Id; + Prag : Node_Id; + + begin + -- Process the contract + + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Post_Nam then + Append_Enabled_Item + (Item => Build_Pragma_Check_Equivalent (Prag), + List => Stmts); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end if; + + -- The subprogram body being processed is actually the proper body + -- of a stub with a corresponding spec. The subprogram stub may + -- carry a postcondition pragma in which case it must be taken + -- into account. The pragma appears after the stub. + + if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then + Decl := Next (Corresponding_Stub (Unit_Decl)); while Present (Decl) loop -- Note that non-matching pragmas are skipped if Nkind (Decl) = N_Pragma then if Pragma_Name (Decl) = Post_Nam then - if not Analyzed (Decl) then - Analyze (Decl); - end if; - - Check_Prag := Build_Pragma_Check_Equivalent (Decl); - - if Expander_Active then - Append_Enabled_Item - (Item => Check_Prag, - List => Stmts); - - -- If analyzing a generic unit, save pragma for later - - else - Prepend_To_Declarations (Check_Prag); - end if; + Append_Enabled_Item + (Item => Build_Pragma_Check_Equivalent (Decl), + List => Stmts); end if; -- Skip internally generated code @@ -7353,157 +7351,118 @@ Next (Decl); end loop; - end Collect_Body_Postconditions_In_Decls; + end if; + end Process_Body_Postconditions; - -- Local variables + --------------------------------- + -- Process_Spec_Postconditions -- + --------------------------------- - Unit_Decl : constant Node_Id := Parent (N); + procedure Process_Spec_Postconditions is + Subps : constant Subprogram_List := + Inherited_Subprograms (Spec_Id); + Items : Node_Id; + Prag : Node_Id; + Subp_Id : Entity_Id; - -- Start of processing for Collect_Body_Postconditions_Of_Kind - begin - pragma Assert (Nam_In (Post_Nam, Name_Postcondition, - Name_Refined_Post)); + -- Process the contract - -- Inspect the declarations of the subprogram body looking for a - -- pragma that matches the desired name. + Items := Contract (Spec_Id); - Collect_Body_Postconditions_In_Decls - (First_Decl => First (Declarations (N))); + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Postcondition then + Append_Enabled_Item + (Item => Build_Pragma_Check_Equivalent (Prag), + List => Stmts); + end if; - -- The subprogram body being processed is actually the proper body - -- of a stub with a corresponding spec. The subprogram stub may - -- carry a postcondition pragma in which case it must be taken - -- into account. The pragma appears after the stub. - - if Present (Spec_Id) and then Nkind (Unit_Decl) = N_Subunit then - Collect_Body_Postconditions_In_Decls - (First_Decl => Next (Corresponding_Stub (Unit_Decl))); + Prag := Next_Pragma (Prag); + end loop; end if; - end Collect_Body_Postconditions_Of_Kind; - -- Start of processing for Collect_Body_Postconditions + -- Process the contracts of all inherited subprograms, looking for + -- class-wide postconditions. - begin - Collect_Body_Postconditions_Of_Kind (Name_Refined_Post); - Collect_Body_Postconditions_Of_Kind (Name_Postcondition); - end Collect_Body_Postconditions; + for Index in Subps'Range loop + Subp_Id := Subps (Index); + Items := Contract (Subp_Id); - --------------------------------- - -- Collect_Spec_Postconditions -- - --------------------------------- + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Postcondition + and then Class_Present (Prag) + then + Append_Enabled_Item + (Item => + Build_Pragma_Check_Equivalent + (Prag => Prag, + Subp_Id => Spec_Id, + Inher_Id => Subp_Id), + List => Stmts); + end if; - procedure Collect_Spec_Postconditions - (Subp_Id : Entity_Id; - Stmts : in out List_Id) - is - Inher_Subps : constant Subprogram_List := - Inherited_Subprograms (Subp_Id); - Check_Prag : Node_Id; - Prag : Node_Id; - Inher_Subp_Id : Entity_Id; - - begin - -- Process the contract of the spec - - Prag := Pre_Post_Conditions (Contract (Subp_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Postcondition then - Check_Prag := Build_Pragma_Check_Equivalent (Prag); - - if Expander_Active then - Append_Enabled_Item - (Item => Check_Prag, - List => Stmts); - - -- When analyzing a generic unit, save the pragma for later - - else - Prepend_To_Declarations (Check_Prag); + Prag := Next_Pragma (Prag); + end loop; end if; - end if; + end loop; + end Process_Spec_Postconditions; - Prag := Next_Pragma (Prag); - end loop; + -- Start of processing for Process_Postconditions - -- Process the contracts of all inherited subprograms, looking for - -- class-wide postconditions. + begin + -- The processing of postconditions is done in reverse order (body + -- first) to ensure the following arrangement: - for Index in Inher_Subps'Range loop - Inher_Subp_Id := Inher_Subps (Index); + -- + -- + -- + -- - Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Postcondition - and then Class_Present (Prag) - then - Check_Prag := - Build_Pragma_Check_Equivalent - (Prag => Prag, - Subp_Id => Subp_Id, - Inher_Id => Inher_Subp_Id); + Process_Body_Postconditions (Name_Refined_Post); + Process_Body_Postconditions (Name_Postcondition); - if Expander_Active then - Append_Enabled_Item - (Item => Check_Prag, - List => Stmts); + if Present (Spec_Id) then + Process_Spec_Postconditions; + end if; + end Process_Postconditions; - -- When analyzing a generic unit, save the pragma for later + --------------------------- + -- Process_Preconditions -- + --------------------------- - else - Prepend_To_Declarations (Check_Prag); - end if; - end if; - - Prag := Next_Pragma (Prag); - end loop; - end loop; - end Collect_Spec_Postconditions; - - -------------------------------- - -- Collect_Spec_Preconditions -- - -------------------------------- - - procedure Collect_Spec_Preconditions (Subp_Id : Entity_Id) is + procedure Process_Preconditions is Class_Pre : Node_Id := Empty; - -- The sole class-wide precondition pragma that applies to the - -- subprogram. + -- The sole [inherited] class-wide precondition pragma that applies + -- to the subprogram. - procedure Add_Or_Save_Precondition (Prag : Node_Id); - -- Save a class-wide precondition or add a regulat precondition to - -- the declarative list of the body. + Insert_Node : Node_Id := Empty; + -- The insertion node after which all pragma Check equivalents are + -- inserted. procedure Merge_Preconditions (From : Node_Id; Into : Node_Id); -- Merge two class-wide preconditions by "or else"-ing them. The -- changes are accumulated in parameter Into. Update the error -- message of Into. - ------------------------------ - -- Add_Or_Save_Precondition -- - ------------------------------ + procedure Prepend_To_Decls (Item : Node_Id); + -- Prepend a single item to the declarations of the subprogram body - procedure Add_Or_Save_Precondition (Prag : Node_Id) is - Check_Prag : Node_Id; + procedure Prepend_To_Decls_Or_Save (Prag : Node_Id); + -- Save a class-wide precondition into Class_Pre or prepend a normal + -- precondition ot the declarations of the body and analyze it. - begin - Check_Prag := Build_Pragma_Check_Equivalent (Prag); + procedure Process_Inherited_Preconditions; + -- Collect all inherited class-wide preconditions and merge them into + -- one big precondition to be evaluated as pragma Check. - -- Save the sole class-wide precondition (if any) for the next - -- step where it will be merged with inherited preconditions. + procedure Process_Preconditions_For (Subp_Id : Entity_Id); + -- Collect all preconditions of subprogram Subp_Id and prepend their + -- pragma Check equivalents to the declarations of the body. - if Class_Present (Prag) then - pragma Assert (No (Class_Pre)); - Class_Pre := Check_Prag; - - -- Accumulate the corresponding Check pragmas to the top of the - -- declarations. Prepending the items ensures that they will be - -- evaluated in their original order. - - else - Prepend_To_Declarations (Check_Prag); - end if; - end Add_Or_Save_Precondition; - ------------------------- -- Merge_Preconditions -- ------------------------- @@ -7576,189 +7535,291 @@ end if; end Merge_Preconditions; - -- Local variables + ---------------------- + -- Prepend_To_Decls -- + ---------------------- - Inher_Subps : constant Subprogram_List := - Inherited_Subprograms (Subp_Id); - Subp_Decl : constant Node_Id := Parent (Parent (Subp_Id)); - Check_Prag : Node_Id; - Decl : Node_Id; - Inher_Subp_Id : Entity_Id; - Prag : Node_Id; + procedure Prepend_To_Decls (Item : Node_Id) is + Decls : List_Id := Declarations (N); - -- Start of processing for Collect_Spec_Preconditions + begin + -- Ensure that the body has a declarative list - begin - -- Process the contract of the spec + if No (Decls) then + Decls := New_List; + Set_Declarations (N, Decls); + end if; - Prag := Pre_Post_Conditions (Contract (Subp_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition then - Add_Or_Save_Precondition (Prag); + Prepend_To (Decls, Item); + end Prepend_To_Decls; + + ------------------------------ + -- Prepend_To_Decls_Or_Save -- + ------------------------------ + + procedure Prepend_To_Decls_Or_Save (Prag : Node_Id) is + Check_Prag : Node_Id; + + begin + Check_Prag := Build_Pragma_Check_Equivalent (Prag); + + -- Save the sole class-wide precondition (if any) for the next + -- step where it will be merged with inherited preconditions. + + if Class_Present (Prag) then + pragma Assert (No (Class_Pre)); + Class_Pre := Check_Prag; + + -- Accumulate the corresponding Check pragmas at the top of the + -- declarations. Prepending the items ensures that they will be + -- evaluated in their original order. + + else + if Present (Insert_Node) then + Insert_After (Insert_Node, Check_Prag); + else + Prepend_To_Decls (Check_Prag); + end if; + + Analyze (Check_Prag); end if; + end Prepend_To_Decls_Or_Save; - Prag := Next_Pragma (Prag); - end loop; + ------------------------------------- + -- Process_Inherited_Preconditions -- + ------------------------------------- - -- The subprogram declaration being processed is actually a body - -- stub. The stub may carry a precondition pragma in which case it - -- must be taken into account. The pragma appears after the stub. + procedure Process_Inherited_Preconditions is + Subps : constant Subprogram_List := + Inherited_Subprograms (Spec_Id); + Check_Prag : Node_Id; + Items : Node_Id; + Prag : Node_Id; + Subp_Id : Entity_Id; - if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then + begin + -- Process the contracts of all inherited subprograms, looking for + -- class-wide preconditions. - -- Inspect the declarations following the body stub + for Index in Subps'Range loop + Subp_Id := Subps (Index); + Items := Contract (Subp_Id); - Decl := Next (Subp_Decl); - while Present (Decl) loop + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Precondition + and then Class_Present (Prag) + then + Check_Prag := + Build_Pragma_Check_Equivalent + (Prag => Prag, + Subp_Id => Spec_Id, + Inher_Id => Subp_Id); - -- Note that non-matching pragmas are skipped + -- The spec or an inherited subprogram already yielded + -- a class-wide precondition. Merge the existing + -- precondition with the current one using "or else". - if Nkind (Decl) = N_Pragma then - if Pragma_Name (Decl) = Name_Precondition then - if not Analyzed (Decl) then - Analyze (Decl); + if Present (Class_Pre) then + Merge_Preconditions (Check_Prag, Class_Pre); + else + Class_Pre := Check_Prag; + end if; end if; - Add_Or_Save_Precondition (Decl); + Prag := Next_Pragma (Prag); + end loop; + end if; + end loop; + + -- Add the merged class-wide preconditions + + if Present (Class_Pre) then + Prepend_To_Decls (Class_Pre); + Analyze (Class_Pre); + end if; + end Process_Inherited_Preconditions; + + ------------------------------- + -- Process_Preconditions_For -- + ------------------------------- + + procedure Process_Preconditions_For (Subp_Id : Entity_Id) is + Items : constant Node_Id := Contract (Subp_Id); + Decl : Node_Id; + Prag : Node_Id; + Subp_Decl : Node_Id; + + begin + -- Process the contract + + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + if Pragma_Name (Prag) = Name_Precondition then + Prepend_To_Decls_Or_Save (Prag); end if; - -- Skip internally generated code + Prag := Next_Pragma (Prag); + end loop; + end if; - elsif not Comes_From_Source (Decl) then - null; + -- The subprogram declaration being processed is actually a body + -- stub. The stub may carry a precondition pragma in which case it + -- must be taken into account. The pragma appears after the stub. - -- Preconditions are usually grouped together. There is no need - -- to inspect the whole declarative list. + Subp_Decl := Unit_Declaration_Node (Subp_Id); - else - exit; - end if; + if Nkind (Subp_Decl) = N_Subprogram_Body_Stub then - Next (Decl); - end loop; - end if; + -- Inspect the declarations following the body stub - -- Process the contracts of all inherited subprograms, looking for - -- class-wide preconditions. + Decl := Next (Subp_Decl); + while Present (Decl) loop - for Index in Inher_Subps'Range loop - Inher_Subp_Id := Inher_Subps (Index); + -- Note that non-matching pragmas are skipped - Prag := Pre_Post_Conditions (Contract (Inher_Subp_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Precondition - and then Class_Present (Prag) - then - Check_Prag := - Build_Pragma_Check_Equivalent - (Prag => Prag, - Subp_Id => Subp_Id, - Inher_Id => Inher_Subp_Id); + if Nkind (Decl) = N_Pragma then + if Pragma_Name (Decl) = Name_Precondition then + Prepend_To_Decls_Or_Save (Decl); + end if; - -- The spec or an inherited subprogram already yielded a - -- class-wide precondition. Merge the existing precondition - -- with the current one using "or else". + -- Skip internally generated code - if Present (Class_Pre) then - Merge_Preconditions (Check_Prag, Class_Pre); + elsif not Comes_From_Source (Decl) then + null; + -- Preconditions are usually grouped together. There is no + -- need to inspect the whole declarative list. + else - Class_Pre := Check_Prag; + exit; end if; - end if; - Prag := Next_Pragma (Prag); - end loop; - end loop; + Next (Decl); + end loop; + end if; + end Process_Preconditions_For; - -- Add the merged class-wide preconditions (if any) + -- Local variables - if Present (Class_Pre) then - Prepend_To_Declarations (Class_Pre); - end if; - end Collect_Spec_Preconditions; + Decls : constant List_Id := Declarations (N); + Decl : Node_Id; - ----------------------------- - -- Prepend_To_Declarations -- - ----------------------------- + -- Start of processing for Process_Preconditions - procedure Prepend_To_Declarations (Item : Node_Id) is - Decls : List_Id := Declarations (N); - begin - -- Ensure that the body has a declarative list + -- Find the last internally generate declaration starting from the + -- top of the body declarations. This ensures that discriminals and + -- subtypes are properly visible to the pragma Check equivalents. - if No (Decls) then - Decls := New_List; - Set_Declarations (N, Decls); + if Present (Decls) then + Decl := First (Decls); + + while Present (Decl) loop + if not Comes_From_Source (Decl) then + Insert_Node := Decl; + exit; + end if; + + Next (Decl); + end loop; end if; - Prepend_To (Decls, Item); - end Prepend_To_Declarations; + -- The processing of preconditions is done in reverse order (body + -- first) because each pragma Check equivalent is inserted at the + -- top of the declarations. This ensures that the final order is + -- consistent with following diagram: - ---------------------------- - -- Process_Contract_Cases -- - ---------------------------- + -- + -- + -- - procedure Process_Contract_Cases - (Subp_Id : Entity_Id; - Stmts : in out List_Id) - is - Prag : Node_Id; + Process_Preconditions_For (Body_Id); - begin - -- Do not build the Contract_Cases circuitry if no code is being - -- generated. - - if not Expander_Active then - return; + if Present (Spec_Id) then + Process_Preconditions_For (Spec_Id); + Process_Inherited_Preconditions; end if; + end Process_Preconditions; - Prag := Contract_Test_Cases (Contract (Subp_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Contract_Cases then - Expand_Contract_Cases - (CCs => Prag, - Subp_Id => Subp_Id, - Decls => Declarations (N), - Stmts => Stmts); - end if; - - Prag := Next_Pragma (Prag); - end loop; - end Process_Contract_Cases; - -- Local variables - Post_Stmts : List_Id := No_List; - Result : Entity_Id; - Subp_Id : Entity_Id; + Restore_Scope : Boolean := False; + Result : Entity_Id; + Stmts : List_Id := No_List; + Subp_Id : Entity_Id; -- Start of processing for Expand_Subprogram_Contract begin + -- Obtain the entity of the initial declaration + if Present (Spec_Id) then Subp_Id := Spec_Id; else Subp_Id := Body_Id; end if; - -- Do not process a predicate function as its body will end up with a - -- recursive call to itself and blow up the stack. + -- Do not perform expansion activity when it is not needed - if Ekind (Subp_Id) = E_Function - and then Is_Predicate_Function (Subp_Id) - then + if not Expander_Active then return; - -- Do not process TSS subprograms + -- ASIS requires an unaltered tree - elsif Get_TSS_Name (Subp_Id) /= TSS_Null then + elsif ASIS_Mode then return; + + -- GNATprove does not need the executable semantics of a contract + + elsif GNATprove_Mode then + return; + + -- The contract of a generic subprogram or one declared in a generic + -- context is not expanded as the corresponding instance will provide + -- the executable semantics of the contract. + + elsif Is_Generic_Subprogram (Subp_Id) or else Inside_A_Generic then + return; + + -- All subprograms carry a contract, but for some it is not significant + -- and should not be processed. This is a small optimization. + + elsif not Has_Significant_Contract (Subp_Id) then + return; end if; - -- The expansion of a subprogram contract involves the relocation of - -- various contract assertions to the declarations of the body in a + -- Do not re-expand the same contract. This scenario occurs when a + -- construct is rewritten into something else during its analysis + -- (expression functions for instance). + + if Has_Expanded_Contract (Subp_Id) then + return; + + -- Otherwise mark the subprogram + + else + Set_Has_Expanded_Contract (Subp_Id); + end if; + + -- Ensure that the formal parameters are visible when expanding all + -- contract items. + + if not In_Open_Scopes (Subp_Id) then + Restore_Scope := True; + Push_Scope (Subp_Id); + + if Is_Generic_Subprogram (Subp_Id) then + Install_Generic_Formals (Subp_Id); + else + Install_Formals (Subp_Id); + end if; + end if; + + -- The expansion of a subprogram contract involves the creation of Check + -- pragmas to verify the contract assertions of the spec and body in a -- particular order. The order is as follows: -- function Example (...) return ... is @@ -7769,14 +7830,13 @@ -- -- -- - -- + -- -- -- end _Postconditions; -- -- -- - -- -- -- @@ -7788,41 +7848,38 @@ -- end Example; -- Routine _Postconditions holds all contract assertions that must be - -- verified on exit from the related routine. + -- verified on exit from the related subprogram. - -- Collect all [inherited] preconditions from the spec, transform them - -- into Check pragmas and add them to the declarations of the body in - -- the order outlined above. + -- Step 1: Handle all preconditions. This action must come before the + -- processing of pragma Contract_Cases because the pragma prepends items + -- to the body declarations. - if Present (Spec_Id) then - Collect_Spec_Preconditions (Spec_Id); - end if; + Process_Preconditions; - -- Transform all [refined] postconditions of the body into Check - -- pragmas. The resulting pragmas are accumulated in list Post_Stmts. + -- Step 2: Handle all postconditions. This action must come before the + -- processing of pragma Contract_Cases because the pragma appends items + -- to list Stmts. - Collect_Body_Postconditions (Post_Stmts); + Process_Postconditions (Stmts); - -- Transform all [inherited] postconditions from the spec into Check - -- pragmas. The resulting pragmas are accumulated in list Post_Stmts. + -- Step 3: Handle pragma Contract_Cases. This action must come before + -- the processing of invariants and predicates because those append + -- items to list Smts. - if Present (Spec_Id) then - Collect_Spec_Postconditions (Spec_Id, Post_Stmts); + Process_Contract_Cases (Stmts); - -- Transform pragma Contract_Cases from the spec into its circuitry + -- Step 4: Apply invariant and predicate checks on a function result and + -- all formals. The resulting checks are accumulated in list Stmts. - Process_Contract_Cases (Spec_Id, Post_Stmts); - end if; + Add_Invariant_And_Predicate_Checks (Subp_Id, Stmts, Result); - -- Apply invariant and predicate checks on the result of a function (if - -- applicable) and all formals. The resulting checks are accumulated in - -- list Post_Stmts. + -- Step 5: Construct procedure _Postconditions - Add_Invariant_And_Predicate_Checks (Subp_Id, Post_Stmts, Result); + Build_Postconditions_Procedure (Subp_Id, Stmts, Result); - -- Construct procedure _Postconditions - - Build_Postconditions_Procedure (Subp_Id, Post_Stmts, Result); + if Restore_Scope then + End_Scope; + end if; end Expand_Subprogram_Contract; -------------------------------- Index: exp_ch6.ads =================================================================== --- exp_ch6.ads (revision 221098) +++ exp_ch6.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -41,17 +41,11 @@ -- This procedure contains common processing for Expand_N_Function_Call, -- Expand_N_Procedure_Statement, and Expand_N_Entry_Call. - procedure Expand_Subprogram_Contract - (N : Node_Id; - Spec_Id : Entity_Id; - Body_Id : Entity_Id); + procedure Expand_Subprogram_Contract (N : Node_Id); -- Expand the contracts of a subprogram body and its correspoding spec (if -- any). This routine processes all [refined] pre- and postconditions as - -- well as Contract_Cases, invariants and predicates. N is the body of the - -- subprogram. Spec_Id denotes the entity of its specification. Body_Id - -- denotes the entity of the subprogram body. This routine is not a "pure" - -- expansion mechanism as it is invoked during analysis and may perform - -- actions for generic subprograms or set up contract assertions for ASIS. + -- well as Contract_Cases, invariants and predicates. N denotes the body of + -- the subprogram. procedure Freeze_Subprogram (N : Node_Id); -- generate the appropriate expansions related to Subprogram freeze Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 221098) +++ sem_ch6.adb (working copy) @@ -104,6 +104,14 @@ -- Local Subprograms -- ----------------------- + procedure Analyze_Function_Return (N : Node_Id); + -- Subsidiary to Analyze_Return_Statement. Called when the return statement + -- applies to a [generic] function. + + procedure Analyze_Generic_Subprogram_Body (N : Node_Id; Gen_Id : Entity_Id); + -- Analyze a generic subprogram body. N is the body to be analyzed, and + -- Gen_Id is the defining entity Id for the corresponding spec. + procedure Analyze_Null_Procedure (N : Node_Id; Is_Completion : out Boolean); @@ -112,10 +120,6 @@ procedure Analyze_Return_Statement (N : Node_Id); -- Common processing for simple and extended return statements - procedure Analyze_Function_Return (N : Node_Id); - -- Subsidiary to Analyze_Return_Statement. Called when the return statement - -- applies to a [generic] function. - procedure Analyze_Return_Type (N : Node_Id); -- Subsidiary to Process_Formals: analyze subtype mark in function -- specification in a context where the formals are visible and hide @@ -125,10 +129,6 @@ -- Does all the real work of Analyze_Subprogram_Body. This is split out so -- that we can use RETURN but not skip the debug output at the end. - procedure Analyze_Generic_Subprogram_Body (N : Node_Id; Gen_Id : Entity_Id); - -- Analyze a generic subprogram body. N is the body to be analyzed, and - -- Gen_Id is the defining entity Id for the corresponding spec. - function Can_Override_Operator (Subp : Entity_Id) return Boolean; -- Returns true if Subp can override a predefined operator. @@ -223,7 +223,7 @@ Check_SPARK_05_Restriction ("abstract subprogram is not allowed", N); Generate_Definition (Designator); - Set_Contract (Designator, Make_Contract (Sloc (Designator))); + Set_Is_Abstract_Subprogram (Designator); New_Overloaded_Entity (Designator); Check_Delayed_Subprogram (Designator); @@ -1266,7 +1266,6 @@ -- Visible generic entity is callable within its own body Set_Ekind (Gen_Id, Ekind (Body_Id)); - Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); Set_Ekind (Body_Id, E_Subprogram_Body); Set_Convention (Body_Id, Convention (Gen_Id)); Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id)); @@ -1316,45 +1315,6 @@ Set_Actual_Subtypes (N, Current_Scope); - -- Deal with [refined] preconditions, postconditions, Contract_Cases, - -- invariants and predicates associated with the body and its spec. - -- Note that this is not pure expansion as Expand_Subprogram_Contract - -- prepares the contract assertions for generic subprograms or for - -- ASIS. Do not generate contract checks in SPARK mode. - - if not GNATprove_Mode then - Expand_Subprogram_Contract (N, Gen_Id, Body_Id); - end if; - - -- If the generic unit carries pre- or post-conditions, copy them - -- to the original generic tree, so that they are properly added - -- to any instantiation. - - declare - Orig : constant Node_Id := Original_Node (N); - Cond : Node_Id; - - begin - Cond := First (Declarations (N)); - while Present (Cond) loop - if Nkind (Cond) = N_Pragma - and then Pragma_Name (Cond) = Name_Check - then - Prepend (New_Copy_Tree (Cond), Declarations (Orig)); - - elsif Nkind (Cond) = N_Pragma - and then Pragma_Name (Cond) = Name_Postcondition - then - Set_Ekind (Defining_Entity (Orig), Ekind (Gen_Id)); - Prepend (New_Copy_Tree (Cond), Declarations (Orig)); - else - exit; - end if; - - Next (Cond); - end loop; - end; - Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Body_Id, True); @@ -1446,7 +1406,6 @@ if Present (Prev) and then Is_Generic_Subprogram (Prev) then Insert_Before (N, Null_Body); Set_Ekind (Defining_Entity (N), Ekind (Prev)); - Set_Contract (Defining_Entity (N), Make_Contract (Loc)); Rewrite (N, Make_Null_Statement (Loc)); Analyze_Generic_Subprogram_Body (Null_Body, Prev); @@ -2191,95 +2150,143 @@ -------------------------------------- procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is - Body_Decl : constant Node_Id := Parent (Parent (Body_Id)); - Mode : SPARK_Mode_Type; - Prag : Node_Id; - Ref_Depends : Node_Id := Empty; - Ref_Global : Node_Id := Empty; - Spec_Id : Entity_Id; + Body_Decl : constant Node_Id := Unit_Declaration_Node (Body_Id); - begin - -- Due to the timing of contract analysis, delayed pragmas may be - -- subject to the wrong SPARK_Mode, usually that of the enclosing - -- context. To remedy this, restore the original SPARK_Mode of the - -- related subprogram body. + procedure Analyze_Completion_Contract (Spec_Id : Entity_Id); + -- Analyze all delayed pragmas chained on the contract of subprogram + -- body Body_Id as if they appeared at the end of a declarative region. + -- Spec_Id denotes the corresponding spec. The aspects in question are: + -- Refined_Depends + -- Refined_Global + -- Note that pragma Refined_Post is analyzed immediately - Save_SPARK_Mode_And_Set (Body_Id, Mode); + --------------------------------- + -- Analyze_Completion_Contract -- + --------------------------------- - -- When a subprogram body declaration is illegal, its defining entity is - -- left unanalyzed. There is nothing left to do in this case because the - -- body lacks a contract, or even a proper Ekind. + procedure Analyze_Completion_Contract (Spec_Id : Entity_Id) is + Items : constant Node_Id := Contract (Body_Id); + Prag : Node_Id; + Prag_Nam : Name_Id; + Ref_Depends : Node_Id := Empty; + Ref_Global : Node_Id := Empty; - if Ekind (Body_Id) = E_Void then - return; - end if; + begin + -- All subprograms carry a contract, but for some it is not + -- significant and should not be processed. - if Nkind (Body_Decl) = N_Subprogram_Body_Stub then - Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); - else - Spec_Id := Corresponding_Spec (Body_Decl); - end if; + if not Has_Significant_Contract (Spec_Id) then + return; - -- Locate and store pragmas Refined_Depends and Refined_Global since - -- their order of analysis matters. + elsif Present (Items) then - Prag := Classifications (Contract (Body_Id)); - while Present (Prag) loop - if Pragma_Name (Prag) = Name_Refined_Depends then - Ref_Depends := Prag; - elsif Pragma_Name (Prag) = Name_Refined_Global then - Ref_Global := Prag; + -- Locate and store pragmas Refined_Depends and Refined_Global + -- since their order of analysis matters. + + Prag := Classifications (Items); + while Present (Prag) loop + Prag_Nam := Pragma_Name (Prag); + + if Prag_Nam = Name_Refined_Depends then + Ref_Depends := Prag; + + elsif Prag_Nam = Name_Refined_Global then + Ref_Global := Prag; + end if; + + Prag := Next_Pragma (Prag); + end loop; end if; - Prag := Next_Pragma (Prag); - end loop; + -- Analyze Refined_Global first as Refined_Depends may mention items + -- classified in the global refinement. - -- Analyze Refined_Global first as Refined_Depends may mention items - -- classified in the global refinement. + if Present (Ref_Global) then + Analyze_Refined_Global_In_Decl_Part (Ref_Global); - if Present (Ref_Global) then - Analyze_Refined_Global_In_Decl_Part (Ref_Global); + -- When the corresponding Global pragma references a state with + -- visible refinement, the body requires Refined_Global. Such a + -- refinement is not required when SPARK checks are suppressed. - -- When the corresponding Global aspect/pragma references a state with - -- visible refinement, the body requires Refined_Global. Refinement is - -- not required when SPARK checks are suppressed. + else + Prag := Get_Pragma (Spec_Id, Pragma_Global); - elsif Present (Spec_Id) then - Prag := Get_Pragma (Spec_Id, Pragma_Global); + if SPARK_Mode /= Off + and then Present (Prag) + and then Contains_Refined_State (Prag) + then + Error_Msg_NE + ("body of subprogram& requires global refinement", + Body_Decl, Spec_Id); + end if; + end if; - if SPARK_Mode /= Off - and then Present (Prag) - and then Contains_Refined_State (Prag) - then - Error_Msg_NE - ("body of subprogram& requires global refinement", - Body_Decl, Spec_Id); + -- Refined_Depends must be analyzed after Refined_Global in order to + -- see the modes of all global refinements. + + if Present (Ref_Depends) then + Analyze_Refined_Depends_In_Decl_Part (Ref_Depends); + + -- When the corresponding Depends pragma references a state with + -- visible refinement, the body requires Refined_Depends. Such a + -- refinement is not required when SPARK checks are suppressed. + + else + Prag := Get_Pragma (Spec_Id, Pragma_Depends); + + if SPARK_Mode /= Off + and then Present (Prag) + and then Contains_Refined_State (Prag) + then + Error_Msg_NE + ("body of subprogram& requires dependance refinement", + Body_Decl, Spec_Id); + end if; end if; + end Analyze_Completion_Contract; + + -- Local variables + + Mode : SPARK_Mode_Type; + Spec_Id : Entity_Id; + + -- Start of processing for Analyze_Subprogram_Body_Contract + + begin + -- When a subprogram body declaration is illegal, its defining entity is + -- left unanalyzed. There is nothing left to do in this case because the + -- body lacks a contract, or even a proper Ekind. + + if Ekind (Body_Id) = E_Void then + return; end if; - -- Refined_Depends must be analyzed after Refined_Global in order to see - -- the modes of all global refinements. + -- Due to the timing of contract analysis, delayed pragmas may be + -- subject to the wrong SPARK_Mode, usually that of the enclosing + -- context. To remedy this, restore the original SPARK_Mode of the + -- related subprogram body. - if Present (Ref_Depends) then - Analyze_Refined_Depends_In_Decl_Part (Ref_Depends); + Save_SPARK_Mode_And_Set (Body_Id, Mode); - -- When the corresponding Depends aspect/pragma references a state with - -- visible refinement, the body requires Refined_Depends. Refinement is - -- not required when SPARK checks are suppressed. + if Nkind (Body_Decl) = N_Subprogram_Body_Stub then + Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl); + else + Spec_Id := Corresponding_Spec (Body_Decl); + end if; - elsif Present (Spec_Id) then - Prag := Get_Pragma (Spec_Id, Pragma_Depends); + -- The subprogram body is a completion, analyze all delayed pragmas that + -- apply. Note that when the body is stand alone, the pragmas are always + -- analyzed on the spot. - if SPARK_Mode /= Off - and then Present (Prag) - and then Contains_Refined_State (Prag) - then - Error_Msg_NE - ("body of subprogram& requires dependance refinement", - Body_Decl, Spec_Id); - end if; + if Present (Spec_Id) then + Analyze_Completion_Contract (Spec_Id); end if; + -- Ensure that the contract cases or postconditions mention 'Result or + -- define a post-state. + + Check_Result_And_Post_State (Body_Id); + -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. @@ -3412,15 +3419,6 @@ end if; end if; - -- Mark presence of postcondition procedure in current scope and mark - -- the procedure itself as needing debug info. The latter is important - -- when analyzing decision coverage (for example, for MC/DC coverage). - - if Chars (Body_Id) = Name_uPostconditions then - Set_Has_Postconditions (Current_Scope); - Set_Debug_Info_Needed (Body_Id); - end if; - -- Place subprogram on scope stack, and make formals visible. If there -- is a spec, the visible entity remains that of the spec. @@ -3591,9 +3589,8 @@ end if; Set_Corresponding_Body (Unit_Declaration_Node (Spec_Id), Body_Id); - Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); - Set_Scope (Body_Id, Scope (Spec_Id)); Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Spec_Id)); + Set_Scope (Body_Id, Scope (Spec_Id)); -- Case of subprogram body with no previous spec @@ -3624,7 +3621,6 @@ if Nkind (N) /= N_Subprogram_Body_Stub then Set_Acts_As_Spec (N); Generate_Definition (Body_Id); - Set_Contract (Body_Id, Make_Contract (Sloc (Body_Id))); Generate_Reference (Body_Id, Body_Id, 'b', Set_Ref => False, Force => True); Install_Formals (Body_Id); @@ -3903,20 +3899,6 @@ Analyze_Aspects_On_Body_Or_Stub; end if; - -- Deal with [refined] preconditions, postconditions, Contract_Cases, - -- invariants and predicates associated with the body and its spec. - -- Note that this is not pure expansion as Expand_Subprogram_Contract - -- prepares the contract assertions for generic subprograms or for ASIS. - -- Do not generate contract checks in SPARK mode. - - if not GNATprove_Mode then - Expand_Subprogram_Contract (N, Spec_Id, Body_Id); - end if; - - -- Analyze the declarations (this call will analyze the precondition - -- Check pragmas we prepended to the list, as well as the declaration - -- of the _Postconditions procedure). - Analyze_Declarations (Declarations (N)); -- Verify that the SPARK_Mode of the body agrees with that of its spec @@ -3946,6 +3928,24 @@ end if; end if; + -- When a subprogram body appears inside a package, its contract is + -- analyzed at the end of the package body declarations. This is due + -- to the delay with respect of the package contract upon which the + -- body contract may depend. When the subprogram body is stand alone + -- and acts as a compilation unit, this delay is not necessary. + + if Nkind (Parent (N)) = N_Compilation_Unit then + Analyze_Subprogram_Body_Contract (Body_Id); + end if; + + -- Deal with preconditions, [refined] postconditions, Contract_Cases, + -- invariants and predicates associated with body and its spec. Since + -- there is no routine Expand_Declarations which would otherwise deal + -- with the contract expansion, generate all necessary mechanisms to + -- verify the contract assertions now. + + Expand_Subprogram_Contract (N); + -- If SPARK_Mode for body is not On, disable frontend inlining for this -- subprogram in GNATprove mode, as its body should not be analyzed. @@ -4163,44 +4163,86 @@ -- Analyze_Subprogram_Contract -- --------------------------------- - procedure Analyze_Subprogram_Contract (Subp : Entity_Id) is - Items : constant Node_Id := Contract (Subp); - Case_Prag : Node_Id := Empty; - Depends : Node_Id := Empty; - Global : Node_Id := Empty; - Mode : SPARK_Mode_Type; - Nam : Name_Id; - Post_Prag : Node_Id := Empty; - Prag : Node_Id; - Seen_In_Case : Boolean := False; - Seen_In_Post : Boolean := False; + procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id) is + procedure Save_Global_References_In_List (First_Prag : Node_Id); + -- Save all global references in contract-related source pragma found in + -- the list starting from pragma First_Prag. + ------------------------------------ + -- Save_Global_References_In_List -- + ------------------------------------ + + procedure Save_Global_References_In_List (First_Prag : Node_Id) is + Prag : Node_Id; + + begin + Prag := First_Prag; + while Present (Prag) loop + if Comes_From_Source (Prag) + and then Nam_In (Pragma_Name (Prag), Name_Contract_Cases, + Name_Depends, + Name_Extensions_Visible, + Name_Global, + Name_Postcondition, + Name_Precondition, + Name_Test_Case) + then + Save_Global_References (Original_Node (Prag)); + end if; + + Prag := Next_Pragma (Prag); + end loop; + end Save_Global_References_In_List; + + -- Local variables + + Items : constant Node_Id := Contract (Subp_Id); + Subp_Decl : constant Node_Id := Unit_Declaration_Node (Subp_Id); + Depends : Node_Id := Empty; + Global : Node_Id := Empty; + Mode : SPARK_Mode_Type; + Prag : Node_Id; + Prag_Nam : Name_Id; + Restore_Scope : Boolean := False; + + -- Start of processing for Analyze_Subprogram_Contract + begin + -- All subprograms carry a contract, but for some it is not significant + -- and should not be processed. + + if not Has_Significant_Contract (Subp_Id) then + return; + end if; + -- Due to the timing of contract analysis, delayed pragmas may be -- subject to the wrong SPARK_Mode, usually that of the enclosing -- context. To remedy this, restore the original SPARK_Mode of the -- related subprogram body. - Save_SPARK_Mode_And_Set (Subp, Mode); + Save_SPARK_Mode_And_Set (Subp_Id, Mode); + -- Ensure that the formal parameters are visible when analyzing all + -- contract items. + + if not In_Open_Scopes (Subp_Id) then + Restore_Scope := True; + Push_Scope (Subp_Id); + + if Is_Generic_Subprogram (Subp_Id) then + Install_Generic_Formals (Subp_Id); + else + Install_Formals (Subp_Id); + end if; + end if; + if Present (Items) then -- Analyze pre- and postconditions Prag := Pre_Post_Conditions (Items); while Present (Prag) loop - Analyze_Pre_Post_Condition_In_Decl_Part (Prag, Subp); - - -- Verify whether a postcondition mentions attribute 'Result and - -- its expression introduces a post-state. - - if Warn_On_Suspicious_Contract - and then Pragma_Name (Prag) = Name_Postcondition - then - Post_Prag := Prag; - Check_Result_And_Post_State (Prag, Seen_In_Post); - end if; - + Analyze_Pre_Post_Condition_In_Decl_Part (Prag); Prag := Next_Pragma (Prag); end loop; @@ -4208,25 +4250,13 @@ Prag := Contract_Test_Cases (Items); while Present (Prag) loop - Nam := Pragma_Name (Prag); + Prag_Nam := Pragma_Name (Prag); - if Nam = Name_Contract_Cases then + if Prag_Nam = Name_Contract_Cases then Analyze_Contract_Cases_In_Decl_Part (Prag); - - -- Verify whether contract-cases mention attribute 'Result and - -- its expression introduces a post-state. Perform the check - -- only when the pragma is legal. - - if Warn_On_Suspicious_Contract - and then not Error_Posted (Prag) - then - Case_Prag := Prag; - Check_Result_And_Post_State (Prag, Seen_In_Case); - end if; - else - pragma Assert (Nam = Name_Test_Case); - Analyze_Test_Case_In_Decl_Part (Prag, Subp); + pragma Assert (Prag_Nam = Name_Test_Case); + Analyze_Test_Case_In_Decl_Part (Prag); end if; Prag := Next_Pragma (Prag); @@ -4236,12 +4266,12 @@ Prag := Classifications (Items); while Present (Prag) loop - Nam := Pragma_Name (Prag); + Prag_Nam := Pragma_Name (Prag); - if Nam = Name_Depends then + if Prag_Nam = Name_Depends then Depends := Prag; - elsif Nam = Name_Global then + elsif Prag_Nam = Name_Global then Global := Prag; -- Note that pragma Extensions_Visible has already been analyzed @@ -4264,51 +4294,42 @@ if Present (Depends) then Analyze_Depends_In_Decl_Part (Depends); end if; + + -- Ensure that the contract cases or postconditions mention 'Result + -- or define a post-state. + + Check_Result_And_Post_State (Subp_Id); end if; - -- Emit an error when neither the postconditions nor the contract-cases - -- mention attribute 'Result in the context of a function. + -- The aspects and contract-related source pragmas associated with a + -- generic subprogram are treated separately from the declaration as + -- they need to be analyzed when the subprogram contract is analyzed. + -- Once this is done, global references can be successfully saved. - if Warn_On_Suspicious_Contract - and then Ekind_In (Subp, E_Function, E_Generic_Function) - then - if Present (Case_Prag) - and then not Seen_In_Case - and then Present (Post_Prag) - and then not Seen_In_Post - then - Error_Msg_N - ("neither function postcondition nor contract cases mention " - & "result?T?", Post_Prag); + if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then - elsif Present (Case_Prag) and then not Seen_In_Case then - Error_Msg_N - ("contract cases do not mention result?T?", Case_Prag); + -- Save all global references found in the aspect specifications of + -- the parameter profile of the generic subprogram. - -- OK if we have at least one IN OUT parameter + Save_Global_References_In_Aspects (Original_Node (Subp_Decl)); - elsif Present (Post_Prag) and then not Seen_In_Post then - declare - F : Entity_Id; - begin - F := First_Formal (Subp); - while Present (F) loop - if Ekind (F) = E_In_Out_Parameter then - return; - else - Next_Formal (F); - end if; - end loop; - end; + -- Save all global references found in contract-related source + -- pragmas. These pragmas usually appear after the declaration of + -- the generic subprogram, either in the same declarative part or + -- in the Pragmas_After list when the generic subprogram is a + -- compilation unit. - -- If no in-out parameters and no mention of Result, the contract - -- is certainly suspicious. - - Error_Msg_N - ("function postcondition does not mention result?T?", Post_Prag); + if Present (Items) then + Save_Global_References_In_List (Pre_Post_Conditions (Items)); + Save_Global_References_In_List (Contract_Test_Cases (Items)); + Save_Global_References_In_List (Classifications (Items)); end if; end if; + if Restore_Scope then + End_Scope; + end if; + -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. @@ -4565,8 +4586,6 @@ Generate_Definition (Designator); end if; - Set_Contract (Designator, Make_Contract (Sloc (Designator))); - if Nkind (N) = N_Function_Specification then Set_Ekind (Designator, E_Function); Set_Mechanism (Designator, Default_Mechanism); @@ -8624,27 +8643,36 @@ and then Is_Subprogram_Or_Generic_Subprogram (E) then declare - Inherited : constant Subprogram_List := Inherited_Subprograms (E); - P : Node_Id; + Subps : constant Subprogram_List := Inherited_Subprograms (E); + Items : Node_Id; + Prag : Node_Id; begin - for J in Inherited'Range loop - P := Pre_Post_Conditions (Contract (Inherited (J))); - while Present (P) loop - Error_Msg_Sloc := Sloc (P); + for Index in Subps'Range loop + Items := Contract (Subps (Index)); - if Class_Present (P) and then not Split_PPC (P) then - if Pragma_Name (P) = Name_Precondition then - Error_Msg_N ("info: & inherits `Pre''Class` aspect " - & "from #?L?", E); - else - Error_Msg_N ("info: & inherits `Post''Class` aspect " - & "from #?L?", E); + if Present (Items) then + Prag := Pre_Post_Conditions (Items); + while Present (Prag) loop + Error_Msg_Sloc := Sloc (Prag); + + if Class_Present (Prag) + and then not Split_PPC (Prag) + then + if Pragma_Name (Prag) = Name_Precondition then + Error_Msg_N + ("info: & inherits `Pre''Class` aspect from " + & "#?L?", E); + else + Error_Msg_N + ("info: & inherits `Post''Class` aspect from " + & "#?L?", E); + end if; end if; - end if; - P := Next_Pragma (P); - end loop; + Prag := Next_Pragma (Prag); + end loop; + end if; end loop; end; end if; Index: sem_ch6.ads =================================================================== --- sem_ch6.ads (revision 221098) +++ sem_ch6.ads (working copy) @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -47,15 +47,22 @@ procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id); -- Analyze all delayed aspects chained on the contract of subprogram body - -- Body_Id as if they appeared at the end of a declarative region. The - -- aspects in question are: + -- Body_Id as if they appeared at the end of a declarative region. Aspects + -- in question are: + -- Contract_Cases (stand alone body) + -- Depends (stand alone body) + -- Global (stand alone body) + -- Postcondition (stand alone body) + -- Precondition (stand alone body) -- Refined_Depends -- Refined_Global + -- Refined_Post + -- Test_Case (stand alone body) - procedure Analyze_Subprogram_Contract (Subp : Entity_Id); - -- Analyze all delayed aspects chained on the contract of subprogram Subp - -- as if they appeared at the end of a declarative region. The aspects in - -- question are: + procedure Analyze_Subprogram_Contract (Subp_Id : Entity_Id); + -- Analyze all delayed aspects chained on the contract of subprogram + -- Subp_Id as if they appeared at the end of a declarative region. The + -- aspects in question are: -- Contract_Cases -- Depends -- Global Index: sem_ch8.adb =================================================================== --- sem_ch8.adb (revision 221100) +++ sem_ch8.adb (working copy) @@ -2871,7 +2871,6 @@ -- constructed later at the freeze point, so indicate that the -- completion has not been seen yet. - Set_Contract (New_S, Empty); Set_Ekind (New_S, E_Subprogram_Body); New_S := Rename_Spec; Set_Has_Completion (Rename_Spec, False); @@ -6459,7 +6458,8 @@ -- is an array type we may already have a usable subtype for it, so we -- can use it rather than generating a new one, because the bounds -- will be the values of the discriminants and not discriminant refs. - -- This simplifies value tracing in GNATProve. + -- This simplifies value tracing in GNATProve. For consistency, both + -- the entity name and the subtype come from the constrained component. function Is_Reference_In_Subunit return Boolean; -- In a subunit, the scope depth is not a proper measure of hiding, @@ -6474,12 +6474,14 @@ function Available_Subtype return Boolean is Comp : Entity_Id; + begin Comp := First_Entity (Etype (P)); while Present (Comp) loop if Chars (Comp) = Chars (Selector_Name (N)) then Set_Etype (N, Etype (Comp)); - Set_Etype (Selector_Name (N), Etype (Comp)); + Set_Entity (Selector_Name (N), Comp); + Set_Etype (Selector_Name (N), Etype (Comp)); return True; end if; Index: sem_warn.adb =================================================================== --- sem_warn.adb (revision 221098) +++ sem_warn.adb (working copy) @@ -40,6 +40,7 @@ with Sem_Ch8; use Sem_Ch8; with Sem_Aux; use Sem_Aux; with Sem_Eval; use Sem_Eval; +with Sem_Prag; use Sem_Prag; with Sem_Util; use Sem_Util; with Sinfo; use Sinfo; with Sinput; use Sinput; @@ -1855,7 +1856,7 @@ if Nkind (P) = N_Pragma and then Pragma_Name (P) = Name_Test_Case - and then Nod = Get_Ensures_From_CTC_Pragma (P) + and then Nod = Test_Case_Arg (P, Name_Ensures) then return True; end if; Index: sem_ch13.adb =================================================================== --- sem_ch13.adb (revision 221098) +++ sem_ch13.adb (working copy) @@ -1257,22 +1257,7 @@ Decl : Node_Id; begin - -- When the context is a library unit, the pragma is added to the - -- Pragmas_After list. - - if Nkind (Parent (N)) = N_Compilation_Unit then - Aux := Aux_Decls_Node (Parent (N)); - - if No (Pragmas_After (Aux)) then - Set_Pragmas_After (Aux, New_List); - end if; - - Prepend (Prag, Pragmas_After (Aux)); - - -- Pragmas associated with subprogram bodies are inserted in the - -- declarative part. - - elsif Nkind (N) = N_Subprogram_Body then + if Nkind (N) = N_Subprogram_Body then if Present (Declarations (N)) then -- Skip other internally generated pragmas from aspects to find @@ -1308,6 +1293,18 @@ Set_Declarations (N, New_List (Prag)); end if; + -- When the context is a library unit, the pragma is added to the + -- Pragmas_After list. + + elsif Nkind (Parent (N)) = N_Compilation_Unit then + Aux := Aux_Decls_Node (Parent (N)); + + if No (Pragmas_After (Aux)) then + Set_Pragmas_After (Aux, New_List); + end if; + + Prepend (Prag, Pragmas_After (Aux)); + -- Default else @@ -2929,7 +2926,7 @@ if not Opt.Exception_Locations_Suppressed then Append_To (Pragma_Argument_Associations (Aitem), Make_Pragma_Argument_Association (Eloc, - Chars => Name_Message, + Chars => Name_Message, Expression => Make_String_Literal (Eloc, Strval => "failed " @@ -2983,7 +2980,6 @@ Comp_Expr := First (Expressions (Expr)); while Present (Comp_Expr) loop New_Expr := Relocate_Node (Comp_Expr); - Set_Original_Node (New_Expr, Comp_Expr); Append_To (Args, Make_Pragma_Argument_Association (Sloc (Comp_Expr), Expression => New_Expr)); @@ -3002,12 +2998,11 @@ goto Continue; end if; - New_Expr := Relocate_Node (Expression (Comp_Assn)); - Set_Original_Node (New_Expr, Expression (Comp_Assn)); Append_To (Args, Make_Pragma_Argument_Association (Sloc (Comp_Assn), - Chars => Chars (First (Choices (Comp_Assn))), - Expression => New_Expr)); + Chars => Chars (First (Choices (Comp_Assn))), + Expression => + Relocate_Node (Expression (Comp_Assn)))); Next (Comp_Assn); end loop;