diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 7b4634c8b5d..eea922d6000 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,23 @@ +2012-12-05 Thomas Quinot + + * par_sco.adb (Traverse_Aspects): Ensure we always have + an entry in the sloc -> SCO map for invariants, since + Set_SCO_Pragma_Enabled is called with that sloc when checks + are enabled. + +2012-12-05 Thomas Quinot + + * exp_ch4.adb: Minor reformatting. + +2012-12-05 Hristian Kirtchev + + * par-prag.adb: Checks and processing of pragma Assume are + carried out by Sem_Prag. + * sem_prag.adb (Analyze_Pragma): Check the legality of pragma + Assume. + * snames.ads-tmpl: Add new name Assume. Add a pragma identifier + for Assume. + 2012-12-05 Ed Schonberg * aspects.ads, aspects.adb: Add aspect Relative_Deadline. diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index 07e7ab8b4b8..b7ecd830048 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -10405,14 +10405,14 @@ package body Exp_Ch4 is -- Convert: x(y) to x'val (ytyp'val (y)) Rewrite (N, - Make_Attribute_Reference (Loc, - Prefix => New_Occurrence_Of (Target_Type, Loc), - Attribute_Name => Name_Val, - Expressions => New_List ( - Make_Attribute_Reference (Loc, - Prefix => New_Occurrence_Of (Operand_Type, Loc), - Attribute_Name => Name_Pos, - Expressions => New_List (Operand))))); + Make_Attribute_Reference (Loc, + Prefix => New_Occurrence_Of (Target_Type, Loc), + Attribute_Name => Name_Val, + Expressions => New_List ( + Make_Attribute_Reference (Loc, + Prefix => New_Occurrence_Of (Operand_Type, Loc), + Attribute_Name => Name_Pos, + Expressions => New_List (Operand))))); Analyze_And_Resolve (N, Target_Type); end if; diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 9d974f3b09a..e1f394b2853 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1093,6 +1093,7 @@ begin when Pragma_Abort_Defer | Pragma_Assertion_Policy | + Pragma_Assume | Pragma_Assume_No_Invalid_Values | Pragma_AST_Entry | Pragma_All_Calls_Remote | diff --git a/gcc/ada/par_sco.adb b/gcc/ada/par_sco.adb index 4ce6951a755..1149a2ec37b 100644 --- a/gcc/ada/par_sco.adb +++ b/gcc/ada/par_sco.adb @@ -493,14 +493,14 @@ package body Par_SCO is begin case T is - when 'I' | 'E' | 'W' | 'a' => + when 'I' | 'E' | 'W' | 'a' | 'A' => -- For IF, EXIT, WHILE, or aspects, the token SLOC is that of -- the parent of the expression. Loc := Sloc (Parent (N)); - if T = 'a' then + if T = 'a' or else T = 'A' then Nam := Chars (Identifier (Parent (N))); end if; @@ -1378,12 +1378,20 @@ package body Par_SCO is procedure Traverse_Aspects (N : Node_Id) is AN : Node_Id; AE : Node_Id; + C1 : Character; begin AN := First (Aspect_Specifications (N)); while Present (AN) loop AE := Expression (AN); + -- SCOs are generated before semantic analysis/expansion: + -- PPCs are not split yet. + + pragma Assert (not Split_PPC (AN)); + + C1 := ASCII.NUL; + case Get_Aspect_Id (Chars (Identifier (AN))) is -- Aspects rewritten into pragmas controlled by a Check_Policy: @@ -1394,37 +1402,24 @@ package body Par_SCO is when Aspect_Pre | Aspect_Precondition | Aspect_Post | - Aspect_Postcondition => + Aspect_Postcondition | + Aspect_Invariant => - -- SCOs are generated before semantic analysis/expansion: - -- PPCs are not split yet. - - pragma Assert (not Split_PPC (AN)); - - -- A Pre/Post aspect will be rewritten into a pragma - -- Precondition/Postcondition with the same sloc. - - pragma Assert (Current_Pragma_Sloc = No_Location); - - Current_Pragma_Sloc := Sloc (AN); - - -- Create the decision as potentially disabled aspect ('a'). - -- Set_SCO_Pragma_Enabled will subsequently switch to 'A'. - - Process_Decisions_Defer (AE, 'a'); - Current_Pragma_Sloc := No_Location; + C1 := 'a'; -- Aspects whose checks are generated in client units, -- regardless of whether or not the check is activated in the - -- unit which contains the declaration. + -- unit which contains the declaration: create decision as + -- unconditionally enabled aspect (but still make a pragma + -- entry since Set_SCO_Pragma_Enabled will be called when + -- analyzing actual checks, possibly in other units). when Aspect_Predicate | Aspect_Static_Predicate | Aspect_Dynamic_Predicate | - Aspect_Invariant | Aspect_Type_Invariant => - Process_Decisions_Defer (AE, 'A'); + C1 := 'A'; -- Other aspects: just process any decision nested in the -- aspect expression. @@ -1432,11 +1427,23 @@ package body Par_SCO is when others => if Has_Decision (AE) then - Process_Decisions_Defer (AE, 'X'); + C1 := 'X'; end if; end case; + if C1 /= ASCII.NUL then + pragma Assert (Current_Pragma_Sloc = No_Location); + + if C1 = 'a' or else C1 = 'A' then + Current_Pragma_Sloc := Sloc (AN); + end if; + + Process_Decisions_Defer (AE, C1); + + Current_Pragma_Sloc := No_Location; + end if; + Next (AN); end loop; end Traverse_Aspects; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index be5afe028a6..36251b8bad1 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2233,6 +2233,18 @@ package body Sem_Prag is (Get_Pragma_Arg (Arg2), Standard_String); end if; + -- For a pragma in the extended main source unit, record enabled + -- status in SCO. + + -- This may seem redundant with the call to Check_Enabled occurring + -- later on when the pragma is rewritten into a pragma Check but + -- is actually required in the case of a postcondition within a + -- generic. + + if Check_Enabled (Pname) and then not Split_PPC (N) then + Set_SCO_Pragma_Enabled (Loc); + end if; + -- If we are within an inlined body, the legality of the pragma -- has been checked already. @@ -6995,6 +7007,21 @@ package body Sem_Prag is Opt.Check_Policy_List := N; end Assertion_Policy; + ------------ + -- Assume -- + ------------ + + -- pragma Assume (boolean_EXPRESSION); + + when Pragma_Assume => Assume : declare + begin + GNAT_Pragma; + S14_Pragma; + Check_Arg_Count (1); + + Analyze_And_Resolve (Expression (Arg1), Any_Boolean); + end Assume; + ------------------------------ -- Assume_No_Invalid_Values -- ------------------------------ @@ -15668,6 +15695,7 @@ package body Sem_Prag is Pragma_Assert => -1, Pragma_Assert_And_Cut => -1, Pragma_Assertion_Policy => 0, + Pragma_Assume => 0, Pragma_Assume_No_Invalid_Values => 0, Pragma_Attribute_Definition => +3, Pragma_Asynchronous => -1, diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index cc269a1446c..bffa6004ba7 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -362,6 +362,7 @@ package Snames is Name_Ada_2012 : constant Name_Id := N + $; -- GNAT Name_Annotate : constant Name_Id := N + $; -- GNAT Name_Assertion_Policy : constant Name_Id := N + $; -- Ada 05 + Name_Assume : constant Name_Id := N + $; -- GNAT Name_Assume_No_Invalid_Values : constant Name_Id := N + $; -- GNAT Name_Attribute_Definition : constant Name_Id := N + $; -- GNAT Name_C_Pass_By_Copy : constant Name_Id := N + $; -- GNAT @@ -1660,6 +1661,7 @@ package Snames is Pragma_Ada_2012, Pragma_Annotate, Pragma_Assertion_Policy, + Pragma_Assume, Pragma_Assume_No_Invalid_Values, Pragma_Attribute_Definition, Pragma_C_Pass_By_Copy,