+ ------------
+ -- Result --
+ ------------
+
+ when Attribute_Result => Result : declare
+ CS : Entity_Id := Current_Scope;
+ PS : Entity_Id := Scope (CS);
+
+ begin
+ -- If the enclosing subprogram is always inlined, the enclosing
+ -- postcondition will not be propagated to the expanded call.
+
+ if Has_Pragma_Inline_Always (PS)
+ and then Warn_On_Redundant_Constructs
+ then
+ Error_Msg_N
+ ("postconditions on inlined functions not enforced?", N);
+ end if;
+
+ -- If we are in the scope of a function and in Spec_Expression mode,
+ -- this is likely the prescan of the postcondition pragma, and we
+ -- just set the proper type. If there is an error it will be caught
+ -- when the real Analyze call is done.
+
+ if Ekind (CS) = E_Function
+ and then In_Spec_Expression
+ then
+ -- Check OK prefix
+
+ if Chars (CS) /= Chars (P) then
+ Error_Msg_NE
+ ("incorrect prefix for % attribute, expected &", P, CS);
+ Error_Attr;
+ end if;
+
+ Set_Etype (N, Etype (CS));
+
+ -- If several functions with that name are visible,
+ -- the intended one is the current scope.
+
+ if Is_Overloaded (P) then
+ Set_Entity (P, CS);
+ Set_Is_Overloaded (P, False);
+ end if;
+
+ -- Body case, where we must be inside a generated _Postcondition
+ -- procedure, and the prefix must be on the scope stack, or else
+ -- the attribute use is definitely misplaced. The condition itself
+ -- may have generated transient scopes, and is not necessarily the
+ -- current one.
+
+ else
+ while Present (CS)
+ and then CS /= Standard_Standard
+ loop
+ if Chars (CS) = Name_uPostconditions then
+ exit;
+ else
+ CS := Scope (CS);
+ end if;
+ end loop;
+
+ PS := Scope (CS);
+
+ if Chars (CS) = Name_uPostconditions
+ and then Ekind (PS) = E_Function
+ then
+ -- Check OK prefix
+
+ if Nkind_In (P, N_Identifier, N_Operator_Symbol)
+ and then Chars (P) = Chars (PS)
+ then
+ null;
+
+ -- Within an instance, the prefix designates the local renaming
+ -- of the original generic.
+
+ elsif Is_Entity_Name (P)
+ and then Ekind (Entity (P)) = E_Function
+ and then Present (Alias (Entity (P)))
+ and then Chars (Alias (Entity (P))) = Chars (PS)
+ then
+ null;
+
+ else
+ Error_Msg_NE
+ ("incorrect prefix for % attribute, expected &", P, PS);
+ Error_Attr;
+ end if;
+
+ Rewrite (N,
+ Make_Identifier (Sloc (N),
+ Chars => Name_uResult));
+ Analyze_And_Resolve (N, Etype (PS));
+
+ else
+ Error_Attr
+ ("% attribute can only appear" &
+ " in function Postcondition pragma", P);
+ end if;
+ end if;
+ end Result;
+