This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
Other format: | [Raw text] |
This patch updates the analysis of pragma Refined_State to reject constants which are used as refinement constituents and are either * Part of the visible state of a package * Part of the hidden state of a package, and lack indicator Part_Of. ------------ -- Source -- ------------ -- var.ads package Var with SPARK_Mode, Initializes => Input is Input : Integer := 0; end Var; -- pack.ads with Var; package Pack with SPARK_Mode, Abstract_State => State is procedure Force_Body; private Const_1 : constant Integer := Var.Input; Const_2 : constant Integer := 2 with Part_Of => State; Var_1 : Integer := 1; Var_2 : Integer := 2 with Part_Of => State; package Priv_Pack is Const_3 : constant Integer := Var.Input; Const_4 : constant Integer := 4 with Part_Of => State; Var_3 : Integer := 3; Var_4 : Integer := 4 with Part_Of => State; end Priv_Pack; end Pack; -- pack.adb package body Pack with SPARK_Mode, Refined_State => (State => (Const_1, -- Error Const_2, -- OK Var_1, -- Error Var_2, -- OK Priv_Pack.Const_3, -- Error Priv_Pack.Const_4, -- OK Priv_Pack.Var_3, -- Error Priv_Pack.Var_4, -- OK Const_5, -- OK Const_6, -- OK Body_Pack.Const_7, -- OK Body_Pack.Const_8)) -- OK is Const_5 : constant Integer := Var.Input; Const_6 : constant Integer := 6; package Body_Pack is Const_7 : constant Integer := Var.Input; Const_8 : constant Integer := 8; end Body_Pack; procedure Force_Body is begin null; end Force_Body; end Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnatf pack.adb pack.adb:5:13: cannot use "Const_1" in refinement, constituent is not a hidden state of package "Pack" pack.adb:7:13: cannot use "Var_1" in refinement, constituent is not a hidden state of package "Pack" pack.adb:9:22: cannot use "Const_3" in refinement, constituent is not a hidden state of package "Pack" pack.adb:11:22: cannot use "Var_3" in refinement, constituent is not a hidden state of package "Pack" pack.ads:13:04: indicator Part_Of is required in this context (SPARK RM 7.2.6(2)) pack.ads:13:04: "Var_1" is declared in the private part of package "Pack" pack.ads:20:07: indicator Part_Of is required in this context (SPARK RM 7.2.6(2)) pack.ads:20:07: "Var_3" is declared in the private part of package "Pack" Tested on x86_64-pc-linux-gnu, committed on trunk 2017-12-15 Hristian Kirtchev <kirtchev@adacore.com> * sem_prag.adb (Match_Constituent): Do not quietly accept constants as suitable constituents. * exp_util.adb: Minor reformatting.
Attachment:
difs
Description: Text document
Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
---|---|---|
Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |