r262731 - in /trunk/gcc/ada: ChangeLog contract...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Mon Jul 16 14:12:33 2018
New Revision: 262731

URL: https://gcc.gnu.org/viewcvs?rev=262731&root=gcc&view=rev
Log:
[Ada] Missing error on hidden state in instantiation

This patch modifies the analysis of package contracts to split processing
which is specific to package instantiations on its own. As a result, the
lack of indicator Part_Of can now be properly assessed.

------------
-- Source --
------------

--  gen_pack.ads

generic
package Gen_Pack is
   Pack_Var : Integer := 1;
end Gen_Pack;

--  gen_wrap.ads

with Gen_Pack;

generic
package Gen_Wrap is
   Wrap_Var : Integer := 1;

   package Inst is new Gen_Pack;
end Gen_Wrap;

--  pack.ads

with Gen_Pack;
with Gen_Wrap;

package Pack
  with SPARK_Mode     => On,
       Abstract_State => State
is
   procedure Force_Body;

private
   package OK_Inst_1 is new Gen_Pack                                 --  OK
     with Part_Of => State;                                          --  OK

   package OK_Inst_2 is new Gen_Pack;                                --  OK
   pragma Part_Of (State);                                           --  OK

   package OK_Inst_3 is new Gen_Wrap                                 --  OK
     with Part_Of => State;                                          --  OK

   package OK_Inst_4 is new Gen_Wrap;                                --  OK
   pragma Part_Of (State);

   package Error_Inst_1 is new Gen_Pack;                             --  Error
   package Error_Inst_2 is new Gen_Wrap;                             --  Error
end Pack;

--  pack.adb

package body Pack
  with SPARK_Mode    => On,
       Refined_State =>
         (State => (OK_Inst_1.Pack_Var, OK_Inst_2.Pack_Var,
                    OK_Inst_3.Wrap_Var, OK_Inst_3.Inst.Pack_Var,
                    OK_Inst_4.Wrap_Var, OK_Inst_4.Inst.Pack_Var))
is
   procedure Force_Body is null;
end Pack;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c pack.adb
pack.ads:23:12: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:23:12: "Error_Inst_1" is declared in the private part of package
  "Pack"
pack.ads:24:12: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:24:12: "Error_Inst_2" is declared in the private part of package
  "Pack"

2018-07-16  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* contracts.adb (Analyze_Contracts): Add specialized processing for
	package instantiation contracts.
	(Analyze_Package_Contract): Remove the verification of a missing
	Part_Of indicator.
	(Analyze_Package_Instantiation_Contract): New routine.
	* contracts.ads (Analyze_Package_Contract): Update the comment on
	usage.
	* sem_prag.adb (Check_Missing_Part_Of): Ensure that the entity of the
	instance is being examined when trying to determine whether a package
	instantiation needs a Part_Of indicator.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/contracts.adb
    trunk/gcc/ada/contracts.ads
    trunk/gcc/ada/sem_prag.adb