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 implements the following rules from SPARK RM 6.1.4: For purposes of the rules concerning the Global, Depends, Refined_Global, and Refined_Depends aspects, when any of these aspects are specified for a task unit the task unit's body is considered to be the body of a procedure and the current instance of the task unit is considered to be a formal parameter (of that notional procedure) of mode IN OUT. Similarly, for purposes of the rules concerning the Global, Refined_Global, Depends, and Refined_Depends aspects as they apply to protected operations, the current instance of the enclosing protected unit is considered to be a formal parameter (of mode IN for a protected function, of mode IN OUT otherwise) and a protected entry is considered to be a protected procedure. The patch also introduces the concept of a body "freezing" the contract of its initial declaration. ------------ -- Source -- ------------ -- synchronized_contracts.ads package Synchronized_Contracts with SPARK_Mode, Abstract_State => State is Var : Integer := 1; protected type Prot_Typ_1 is entry Prot_Ent (Formal : out Integer) with Global => (Input => (State, Var)), Depends => ((Prot_Typ_1, Formal) => (State, Var, Prot_Typ_1)); end Prot_Typ_1; protected Prot_Typ_2 is entry Prot_Ent (Formal : out Integer); pragma Global ((Input => State)); pragma Depends ((Formal => State)); end Prot_Typ_2; task type Task_Typ_1 with Global => (Input => State, Output => Var), Depends => ((Var, Task_Typ_1) => (State, Task_Typ_1)); task Task_Typ_2; pragma Global ((Output => (State, Var))); pragma Depends (((State, Var) => null)); end Synchronized_Contracts; -- synchronized_contracts.adb package body Synchronized_Contracts with SPARK_Mode, Refined_State => (State => Constit) is Constit : Integer := 2; protected body Prot_Typ_1 is entry Prot_Ent (Formal : out Integer) when True is pragma Refined_Global ((Input => (Constit, Var))); pragma Refined_Depends (((Prot_Typ_1, Formal) => (Constit, Var, Prot_Typ_1))); begin Formal := Constit + Var; end Prot_Ent; end Prot_Typ_1; protected body Prot_Typ_2 is entry Prot_Ent (Formal : out Integer) with Refined_Global => (Input => Constit), Refined_Depends => (Formal => Constit) when True is begin Formal := Constit + 1; end Prot_Ent; end Prot_Typ_2; task body Task_Typ_1 is pragma Refined_Global ((Input => Constit, Output => Var)); pragma Refined_Depends (((Var, Task_Typ_1) => (Constit, Task_Typ_1))); begin null; end Task_Typ_1; task body Task_Typ_2 with Refined_Global => (Output => (Constit, Var)), Refined_Depends => ((Constit, Var) => null) is begin null; end Task_Typ_2; end Synchronized_Contracts; ----------------- -- Compilation -- ----------------- $ gcc -c synchronized_contracts.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2015-10-26 Hristian Kirtchev <kirtchev@adacore.com> * atree.ads, atree.adb (Ekind_In): New 10 and 11 parameter versions. * contracts.ads, contracts.adb (Analyze_Initial_Declaration_Contract): New routine. * sem_ch6.adb (Analyze_Generic_Subprogram_Body): Analyze the contract of the initial declaration. (Analyze_Subprogram_Body_Helper): Analyze the contract of the initial declaration. * sem_ch7.adb (Analyze_Package_Body_Helper): Analyze the contract of the initial declaration. * sem_ch9.adb (Analyze_Entry_Body): Analyze the contract of the initial declaration. (Analyze_Protected_Body): Analyze the contract of the initial declaration. (Analyze_Task_Body): Analyze the contract of the initial declaration. * sem_prag.adb (Add_Entity_To_Name_Buffer): Use "type" rather than "unit" as it makes the error messages sound better. (Add_Item_To_Name_Buffer): Update comment on usage. The routine now supports discriminants and current instances of concurrent types. (Analyze_Depends_In_Decl_Part): Install the discriminants of a task type. (Analyze_Global_In_Decl_Part): Install the discriminants of a task type. (Analyze_Global_Item): Add processing for current instances of concurrent types and include discriminants as valid global items. (Analyze_Input_Output): Discriminants and current instances of concurrent types are now valid items. Update various error messages. (Check_Usage): Current instances of protected and task types behaves as formal parameters. (Collect_Subprogram_Inputs_Outputs): There is no longer need to manually analyze [Refined_]Global thanks to freezing of initial declaration contracts. Add processing for the current instance of a concurrent type. (Find_Role): Add categorizations for discriminants, protected and task types. (Is_CCT_Instance): New routine. (Match_Items): Update the comment on usage. Update internal comments. * sem_prag.ads (Collect_Subprogram_Inputs_Outputs): Update the comment on usage. * sem_util.adb (Entity_Of): Ensure that the entity is an object when traversing a potential renaming chain. (Fix_Msg): Use "type" rather than "unit" as it makes the error messages sound better. * sem_util.ads (Fix_Msg): Update the comment on usage.
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] |