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 a mechanism which detects missing refinement of abstract states depending on whether a package requires a completing body or not. The patch also cleans up the two entity lists used to store refinement and Part_Of constituents of abstract states. ------------ -- Source -- ------------ -- lib_pack_1.ads package Lib_Pack_1 with SPARK_Mode, Abstract_State => Error_State_1 -- Error is package Nested_1 with Abstract_State => Error_State_2 -- Error is end Nested_1; end Lib_Pack_1; -- lib_pack_2.ads package Lib_Pack_2 with SPARK_Mode, Abstract_State => OK_1 is package Nested_1 with Abstract_State => Error_1 -- Error is end Nested_1; package Nested_2 with Abstract_State => OK_2 is end Nested_2; package Nested_3 with Abstract_State => Error_2 -- Error is end Nested_3; procedure Force_Body; end Lib_Pack_2; -- lib_pack_2.adb package body Lib_Pack_2 with SPARK_Mode, Refined_State => (OK_1 => null) is package body Nested_1 is end Nested_1; package body Nested_2 with Refined_State => (OK_2 => null) is end Nested_2; -- package body Nested_3 is missing procedure Force_Body is begin null; end Force_Body; end Lib_Pack_2; -- non_lib_pack.ads package Non_Lib_Pack with SPARK_Mode is procedure Force_Body; end Non_Lib_Pack; -- non_lib_pack.adb package body Non_Lib_Pack with SPARK_Mode is procedure Force_Body is package Nested_1 with Abstract_State => Error_1 -- Error is end Nested_1; package body Nested_1 is end Nested_1; package Nested_2 with Abstract_State => OK_1 is end Nested_2; package body Nested_2 with Refined_State => (OK_1 => null) -- OK is end Nested_2; package Nested_3 with Abstract_State => Error_2 -- Error is end Nested_3; -- package body Nested_3 is missing begin null; end Force_Body; end Non_Lib_Pack; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c lib_pack_1.ads $ gcc -c lib_pack_2.adb $ gcc -c non_lib_pack.adb lib_pack_1.ads:3:26: state "Error_State_1" requires refinement lib_pack_1.ads:6:29: state "Error_State_2" requires refinement lib_pack_2.ads:6:29: state "Error_1" requires refinement lib_pack_2.ads:16:29: state "Error_2" requires refinement non_lib_pack.adb:4:32: state "Error_1" requires refinement non_lib_pack.adb:22:32: state "Error_2" requires refinement Tested on x86_64-pc-linux-gnu, committed on trunk 2016-04-21 Hristian Kirtchev <kirtchev@adacore.com> * contracts.adb (Analyze_Package_Body_Contract): Do not check for a missing package refinement because 1) packages do not have "refinement" and 2) the check for proper state refinement is performed in a different place. * einfo.adb (Has_Non_Null_Visible_Refinement): Reimplemented. (Has_Null_Visible_Refinement): Reimplemented. * sem_ch3.adb (Analyze_Declarations): Determine whether all abstract states have received a refinement and if not, emit errors. * sem_ch7.adb (Analyze_Package_Declaration): Code cleanup. Determine whether all abstract states of the package and any nested packages have received a refinement and if not, emit errors. (Requires_Completion_In_Body): Add new formal parameter Do_Abstract_States. Update the comment on usage. Propagate the Do_Abstract_States flag to all Unit_Requires_Body calls. (Unit_Requires_Body): Remove formal parameter Ignore_Abstract_States. Add new formal paramter Do_Abstract_States. Propagate the Do_Abstract_States flag to all Requires_Completion_In calls. * sem_ch7.ads (Unit_Requires_Body): Remove formal parameter Ignore_Abstract_States. Add new formal paramter Do_Abstract_States. Update the comment on usage. * sem_ch9.adb (Analyze_Single_Protected_Declaration): Do not initialize the constituent list as this is now done on a need-to-add-element basis. (Analyze_Single_Task_Declaration): Do not initialize the constituent list as this is now done on a need-to-add-element basis. * sem_ch10.adb (Decorate_State): Do not initialize the constituent lists as this is now done on a need-to-add-element basis. * sem_prag.adb (Analyze_Constituent): Set the refinement constituents when adding a new element. (Analyze_Part_Of_In_Decl_Part): Set the Part_Of constituents when adding a new element. (Analyze_Part_Of_Option): Set the Part_Of constituents when adding a new element. (Analyze_Pragma): Set the Part_Of constituents when adding a new element. (Check_Constituent_Usage (all versions)): Reimplemented. (Collect_Constituent): Set the refinement constituents when adding a new element. (Create_Abstract_State): Do not initialize the constituent lists as this is now done on a need-to-add-element basis. (Propagate_Part_Of): Set the Part_Of constituents when adding a new element. * sem_util.adb (Check_State_Refinements): New routine. (Has_Non_Null_Refinement): Reimplemented. (Has_Null_Refinement): Reimplemented. (Requires_State_Refinement): Removed. * sem_util.ads (Check_State_Refinements): New routine. (Requires_State_Refinement): Removed.
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] |