From: Piotr Trojanek Date: Thu, 7 May 2026 14:37:01 +0000 (+0200) Subject: ada: Basic support for a new SPARK attribute At X-Git-Url: http://git.ipfire.org/gitweb/index.cgi?a=commitdiff_plain;h=03d4c76460aae3ebbb4b24d29cbdfb451b651d22;p=thirdparty%2Fgcc.git ada: Basic support for a new SPARK attribute At For now, only basic legality checks are present. Expansion is not ready yet. This should be enough to start implementing the backend support in GNATprove. gcc/ada/ChangeLog: * exp_attr.adb (Expand_N_Attribute_Reference): Do not expand new attribute. * par-ch4.adb (Scan_Apostrophe): Parse 'At as an attribute reference; otherwise, it would be parsed as a keyword. * sem_attr.adb (Analyze_Attribute): Basic checks for new attribute. (Eval_Attribute): New attribute will never be evaluated. * snames.ads-tmpl: (Preset Names): "at" is now also an attribute, not just a keyword. (Attribute_Id): New attribute identifier. --- diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb index 1834ee3d291..8021a591c67 100644 --- a/gcc/ada/exp_attr.adb +++ b/gcc/ada/exp_attr.adb @@ -5437,6 +5437,9 @@ package body Exp_Attr is when Attribute_Loop_Entry => Expand_Loop_Entry_Attribute (N); + when Attribute_At => + Error_Msg_N ("expansion of attribute At is not yet supported", N); + ------------- -- Machine -- ------------- diff --git a/gcc/ada/par-ch4.adb b/gcc/ada/par-ch4.adb index 0a25ac853f7..13328c959e4 100644 --- a/gcc/ada/par-ch4.adb +++ b/gcc/ada/par-ch4.adb @@ -527,6 +527,12 @@ package body Ch4 is elsif Token = Tok_Mod and then Ada_Version >= Ada_95 then Attr_Name := Name_Mod; + elsif Token = Tok_At then + Attr_Name := Name_At; + + Error_Msg_GNAT_Extension + ("attribute At", Token_Ptr, Is_Core_Extension => False); + elsif Apostrophe_Should_Be_Semicolon then Expr_Form := EF_Name; return Name_Node; diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index 86deb65552b..74ad6dac29b 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -3580,6 +3580,144 @@ package body Sem_Attr is Set_Etype (N, RTE (RE_Asm_Output_Operand)); + -------- + -- At -- + -------- + + when Attribute_At => + Check_E1; + + -- Set the type of the attribute now to ensure the successful + -- continuation of analysis even if the attribute is misplaced. + + Set_Etype (N, P_Type); + + -- We start with the same checks as for goto statements. The final + -- check rejects references to forward labels, which are allowed for + -- goto, but not for this attribute. + + if not (Nkind (E1) = N_Identifier + and then Ekind (Entity (E1)) = E_Label) + then + Error_Attr ("label expected", E1); + elsif not Reachable (Entity (E1)) then + Error_Attr ("label is not reachable", E1); + elsif Sloc (E1) < Sloc (Entity (E1)) then + Error_Attr ("forward label reference", E1); + end if; + + declare + function Check_Goto (Stmt : Node_Id) return Traverse_Result; + -- Detect goto statements that "jump over" the attribute label + + function Check_Reference (Ref : Node_Id) return Traverse_Result; + -- Check if reference denotes entity visible at the location of + -- the referenced label or declared within the prefix itself. + + function Declared_Within_Prefix (E : Entity_Id) return Boolean; + -- Return True iff E is declared within the attribute prefix + + Label_Depth : constant Unat := Scope_Depth (Scope (Entity (E1))); + -- Scope depth at the label + + ------------- + -- Check_Goto -- + ------------- + + function Check_Goto (Stmt : Node_Id) return Traverse_Result is + begin + -- Check if the target of a goto statement is located past the + -- label appearing in the attribute expression. + + if Nkind (Stmt) in N_Goto_Statement | N_Goto_When_Statement + and then Sloc (Entity (Name (Stmt))) > Sloc (Entity (E1)) + then + Error_Msg_Sloc := Sloc (Stmt); + Error_Msg_N + ("!attribute label is skipped by goto at #", N); + return Skip; + + -- Stop once we reached the attribute label + + elsif Nkind (Stmt) = N_Label + and then Entity (Identifier (Stmt)) = Entity (E1) + then + return Abandon; + + -- Skip constructs where a goto jump will not be allowed anyway + + elsif Nkind (Stmt) in N_Package_Declaration + | N_Package_Body + | N_Subprogram_Body + | N_Generic_Declaration + | N_Single_Task_Declaration + | N_Task_Type_Declaration + | N_Single_Protected_Declaration + | N_Protected_Type_Declaration + | N_Protected_Body + | N_Task_Body + then + return Skip; + + else + return OK; + end if; + end Check_Goto; + + --------------------- + -- Check_Reference -- + --------------------- + + function Check_Reference (Ref : Node_Id) return Traverse_Result is + begin + -- To check if referenced entity is visible at the label we + -- simply compare the scope depth. + + if Nkind (Ref) = N_Identifier + and then Present (Entity (Ref)) + and then Scope_Depth (Scope (Entity (Ref))) > Label_Depth + and then not Declared_Within_Prefix (Entity (Ref)) + then + Error_Msg_Sloc := Sloc (Entity (E1)); + Error_Msg_NE ("!& is not visible at #", N, Entity (Ref)); + end if; + + return OK; + end Check_Reference; + + ---------------------------- + -- Declared_Within_Prefix -- + ---------------------------- + + function Declared_Within_Prefix (E : Entity_Id) return Boolean is + Context : Node_Id; + + begin + Context := E; + while Present (Context) loop + if Context = P then + return True; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Context) then + return False; + end if; + + Context := Parent (Context); + end loop; + + return False; + end Declared_Within_Prefix; + + procedure Check_Gotos is new Traverse_Proc (Check_Goto); + procedure Check_References is new Traverse_Proc (Check_Reference); + + begin + Check_Gotos (Parent (Label_Construct (Parent (Entity (E1))))); + Check_References (P); + end; + ----------------------------- -- Atomic_Always_Lock_Free -- ----------------------------- @@ -11378,6 +11516,7 @@ package body Sem_Attr is | Attribute_Address_Size | Attribute_Asm_Input | Attribute_Asm_Output + | Attribute_At | Attribute_Base | Attribute_Bit_Order | Attribute_Bit_Position diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 3fa60851c95..30ead95798e 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -947,6 +947,7 @@ package Snames is Name_Alignment : constant Name_Id := N + $; Name_Asm_Input : constant Name_Id := N + $; -- GNAT Name_Asm_Output : constant Name_Id := N + $; -- GNAT + Name_At : constant Name_Id := N + $; -- GNAT Name_Atomic_Always_Lock_Free : constant Name_Id := N + $; -- GNAT Name_Bit : constant Name_Id := N + $; -- GNAT Name_Bit_Order : constant Name_Id := N + $; @@ -1294,7 +1295,6 @@ package Snames is Name_And : constant Name_Id := N + $; Name_All : constant Name_Id := N + $; Name_Array : constant Name_Id := N + $; - Name_At : constant Name_Id := N + $; Name_Begin : constant Name_Id := N + $; Name_Body : constant Name_Id := N + $; Name_Case : constant Name_Id := N + $; @@ -1486,6 +1486,7 @@ package Snames is Attribute_Alignment, Attribute_Asm_Input, Attribute_Asm_Output, + Attribute_At, Attribute_Atomic_Always_Lock_Free, Attribute_Bit, Attribute_Bit_Order,