From 5b5588dd53fd0da82e406f5de6e9f189f89f1b1a Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 2 Sep 2011 11:59:32 +0200 Subject: [PATCH] [multiple changes] 2011-09-02 Bob Duff * sem_ch6.adb: (Check_Post_State): Suppress warning "postcondition refers only to pre-state" when the expression has not yet been analyzed, because it causes false alarms. This can happen when the postcondition contains a quantified expression, because those are analyzed later. This is a temporary/partial fix. (Process_Post_Conditions): Minor: change wording of warning. 2011-09-02 Marc Sango * sem_ch3.adb (Analyze_Object_Declaration): Detect the violation of illegal use of unconstrained string type in SPARK mode. * sem_res.adb (Analyze_Operator_Symbol): Set the right place where the string operand of concatenation should be violate in SPARK mode. From-SVN: r178460 --- gcc/ada/ChangeLog | 17 +++++++++++++++++ gcc/ada/sem_ch3.adb | 9 +++++++++ gcc/ada/sem_ch6.adb | 15 +++++++++++---- gcc/ada/sem_res.adb | 4 ++-- 4 files changed, 39 insertions(+), 6 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 91b2ebf4aa9..4ca7037e877 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,20 @@ +2011-09-02 Bob Duff + + * sem_ch6.adb: (Check_Post_State): Suppress warning + "postcondition refers only to pre-state" when the expression has not + yet been analyzed, because it causes false alarms. This can happen when + the postcondition contains a quantified expression, because those are + analyzed later. This is a temporary/partial fix. + (Process_Post_Conditions): Minor: change wording of warning. + +2011-09-02 Marc Sango + + * sem_ch3.adb (Analyze_Object_Declaration): Detect the violation of + illegal use of unconstrained string type in SPARK mode. + * sem_res.adb (Analyze_Operator_Symbol): Set the + right place where the string operand of concatenation should be + violate in SPARK mode. + 2011-09-02 Robert Dewar * sem_prag.adb, sem_util.adb, sem_ch6.adb, prj-nmsc.adb, diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 4102bea4378..fb702f31f4a 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3313,9 +3313,18 @@ package body Sem_Ch3 is -- Case of initialization present else + -- Not allowed in Ada 83 if not Constant_Present (N) then + + -- A declaration of unconstrained type in SPARK is limited, + -- the only exception to this is the admission of declaration + -- of constants of type string. + + Check_SPARK_Restriction + ("declaration of unconstrained type is limited", E); + if Ada_Version = Ada_83 and then Comes_From_Source (Object_Definition (N)) then diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 32c2dbbe9c3..bd1b6e34d3b 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -5551,9 +5551,16 @@ package body Sem_Ch6 is declare E : constant Entity_Id := Entity (N); begin - if Is_Entity_Name (N) - and then Present (E) - and then Ekind (E) in Assignable_Kind + -- ???Quantified expressions get analyzed later, so E can be + -- empty at this point. In this case, we suppress the + -- warning, just in case E is assignable. It seems better to + -- have false negatives than false positives. At some point, + -- we should make the warning more accurate, either by + -- analyzing quantified expressions earlier, or moving this + -- processing later. + + if No (E) or else + (Is_Entity_Name (N) and then Ekind (E) in Assignable_Kind) then Found := True; end if; @@ -5627,7 +5634,7 @@ package body Sem_Ch6 is Ignored := Find_Post_State (Arg); if not Post_State_Mentioned then - Error_Msg_N ("?postcondition only refers to pre-state", + Error_Msg_N ("?postcondition refers only to pre-state", Prag); end if; end if; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 7668aa9e217..0a15075994c 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7741,7 +7741,7 @@ package body Sem_Res is if Is_Character_Type (Etype (Arg)) then if not Is_Static_Expression (Arg) then Check_SPARK_Restriction - ("character operand for concatenation should be static", N); + ("character operand for concatenation should be static", Arg); end if; elsif Is_String_Type (Etype (Arg)) then @@ -7750,7 +7750,7 @@ package body Sem_Res is and then not Is_Static_Expression (Arg) then Check_SPARK_Restriction - ("string operand for concatenation should be static", N); + ("string operand for concatenation should be static", Arg); end if; -- Do not issue error on an operand that is neither a character nor a -- 2.30.2