From: charlet Date: Wed, 29 Jan 2014 15:21:59 +0000 (+0000) Subject: 2014-01-29 Tristan Gingold X-Git-Url: http://git.ipfire.org/?a=commitdiff_plain;h=8325ff3be4b110a27bd59a6567bf32d6a0452b43;p=thirdparty%2Fgcc.git 2014-01-29 Tristan Gingold * exp_ch9.adb (Is_Exception_Safe): Return true if no exceptions. 2014-01-29 Yannick Moy * inline.ads (Pending_Body_Info): Add SPARK_Mode and SPARK_Mode_Pragma components to be able to analyze generic instance. * sem_ch12.adb (Analyze_Package_Instantiation, Inline_Instance_Body, Need_Subprogram_Instance_Body, Load_Parent_Of_Generic): Pass in SPARK_Mode from instantiation for future analysis of the instance. (Instantiate_Package_Body, Instantiate_Subprogram_Body, Set_Instance_Inv): Set SPARK_Mode from instantiation to analyze the instance. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@207244 138bc75d-0d04-0410-961f-82ee72b054a4 --- diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 23fc4021aca4..cdef61ed1edf 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2014-01-29 Tristan Gingold + + * exp_ch9.adb (Is_Exception_Safe): Return true if no exceptions. + +2014-01-29 Yannick Moy + + * inline.ads (Pending_Body_Info): Add SPARK_Mode and + SPARK_Mode_Pragma components to be able to analyze generic + instance. + * sem_ch12.adb (Analyze_Package_Instantiation, + Inline_Instance_Body, Need_Subprogram_Instance_Body, + Load_Parent_Of_Generic): Pass in SPARK_Mode from instantiation + for future analysis of the instance. + (Instantiate_Package_Body, + Instantiate_Subprogram_Body, Set_Instance_Inv): Set SPARK_Mode + from instantiation to analyze the instance. + 2014-01-29 Robert Dewar * sem_ch7.adb, sem_prag.adb, sem_ch4.adb, sem_ch6.adb: Minor code diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb index 694569ddc24c..8f78f0619f77 100644 --- a/gcc/ada/exp_ch9.adb +++ b/gcc/ada/exp_ch9.adb @@ -13425,6 +13425,14 @@ package body Exp_Ch9 is -- Start of processing for Is_Exception_Safe begin + + -- When exceptions can not be propagated, the subprogram will always + -- return normaly. + + if No_Exception_Handlers_Set then + return True; + end if; + -- If the checks handled by the back end are not disabled, we cannot -- ensure that no exception will be raised. diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads index 825b958f1ef0..fd0e965f3f23 100644 --- a/gcc/ada/inline.ads +++ b/gcc/ada/inline.ads @@ -96,6 +96,11 @@ package Inline is Warnings : Warning_Record; -- Capture values of warning flags + + SPARK_Mode : SPARK_Mode_Type; + SPARK_Mode_Pragma : Node_Id; + -- SPARK_Mode for an instance is the one applicable at the point of + -- instantiation. end record; package Pending_Instantiations is new Table.Table ( diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 565df4edf078..c9adaaca353a 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3899,7 +3899,9 @@ package body Sem_Ch12 is Local_Suppress_Stack_Top => Local_Suppress_Stack_Top, Version => Ada_Version, Version_Pragma => Ada_Version_Pragma, - Warnings => Save_Warnings)); + Warnings => Save_Warnings, + SPARK_Mode => SPARK_Mode, + SPARK_Mode_Pragma => SPARK_Mode_Pragma)); end if; end if; @@ -4245,7 +4247,9 @@ package body Sem_Ch12 is Local_Suppress_Stack_Top => Local_Suppress_Stack_Top, Version => Ada_Version, Version_Pragma => Ada_Version_Pragma, - Warnings => Save_Warnings)), + Warnings => Save_Warnings, + SPARK_Mode => SPARK_Mode, + SPARK_Mode_Pragma => SPARK_Mode_Pragma)), Inlined_Body => True); Pop_Scope; @@ -4363,7 +4367,9 @@ package body Sem_Ch12 is Local_Suppress_Stack_Top => Local_Suppress_Stack_Top, Version => Ada_Version, Version_Pragma => Ada_Version_Pragma, - Warnings => Save_Warnings)), + Warnings => Save_Warnings, + SPARK_Mode => SPARK_Mode, + SPARK_Mode_Pragma => SPARK_Mode_Pragma)), Inlined_Body => True); end if; end Inline_Instance_Body; @@ -4421,7 +4427,9 @@ package body Sem_Ch12 is Local_Suppress_Stack_Top => Local_Suppress_Stack_Top, Version => Ada_Version, Version_Pragma => Ada_Version_Pragma, - Warnings => Save_Warnings)); + Warnings => Save_Warnings, + SPARK_Mode => SPARK_Mode, + SPARK_Mode_Pragma => SPARK_Mode_Pragma)); return True; -- Here if not inlined, or we ignore the inlining @@ -9913,6 +9921,8 @@ package body Sem_Ch12 is Opt.Ada_Version := Body_Info.Version; Opt.Ada_Version_Pragma := Body_Info.Version_Pragma; Restore_Warnings (Body_Info.Warnings); + Opt.SPARK_Mode := Body_Info.SPARK_Mode; + Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma; if No (Gen_Body_Id) then Load_Parent_Of_Generic @@ -10203,6 +10213,8 @@ package body Sem_Ch12 is Opt.Ada_Version := Body_Info.Version; Opt.Ada_Version_Pragma := Body_Info.Version_Pragma; Restore_Warnings (Body_Info.Warnings); + Opt.SPARK_Mode := Body_Info.SPARK_Mode; + Opt.SPARK_Mode_Pragma := Body_Info.SPARK_Mode_Pragma; if No (Gen_Body_Id) then @@ -12091,7 +12103,9 @@ package body Sem_Ch12 is Local_Suppress_Stack_Top, Version => Ada_Version, Version_Pragma => Ada_Version_Pragma, - Warnings => Save_Warnings); + Warnings => Save_Warnings, + SPARK_Mode => SPARK_Mode, + SPARK_Mode_Pragma => SPARK_Mode_Pragma); -- Package instance @@ -12133,7 +12147,9 @@ package body Sem_Ch12 is Local_Suppress_Stack_Top => Local_Suppress_Stack_Top, Version => Ada_Version, Version_Pragma => Ada_Version_Pragma, - Warnings => Save_Warnings)), + Warnings => Save_Warnings, + SPARK_Mode => SPARK_Mode, + SPARK_Mode_Pragma => SPARK_Mode_Pragma)), Body_Optional => Body_Optional); end; end if; @@ -13799,7 +13815,9 @@ package body Sem_Ch12 is (Gen_Unit : Entity_Id; Act_Unit : Entity_Id) is - Assertion_Status : constant Boolean := Assertions_Enabled; + Assertion_Status : constant Boolean := Assertions_Enabled; + Save_SPARK_Mode : constant SPARK_Mode_Type := SPARK_Mode; + Save_SPARK_Mode_Pragma : constant Node_Id := SPARK_Mode_Pragma; begin -- Regardless of the current mode, predefined units are analyzed in the @@ -13822,6 +13840,12 @@ package body Sem_Ch12 is if Ada_Version >= Ada_2012 then Assertions_Enabled := Assertion_Status; end if; + + -- SPARK_Mode for an instance is the one applicable at the point of + -- instantiation. + + SPARK_Mode := Save_SPARK_Mode; + SPARK_Mode_Pragma := Save_SPARK_Mode_Pragma; end if; Current_Instantiated_Parent :=