+2017-09-08 Yannick Moy <moy@adacore.com>
+
+ * sem_aux.adb, sem_aux.ads (Get_Called_Entity): New function to
+ return the entity associated with the call.
+ * sem_util.adb, sem_util.ads (Check_Function_Writable_Actuals):
+ Replace the internal Get_Function_Id with the new
+ Sem_Aux.Get_Called_Entity.
+ (Iterate_Call_Parameters): New
+ procedure to iterate on formals and actuals at the same time.
+ * sem_ch12.adb (Analyze_Subprogram_Instantiation):
+ Set SPARK_Mode from spec when set, for analysis
+ of instance. Restore after analysis of instance.
+ (Instantiate_Subprogram_Body): Set SPARK_Mode from body when
+ set, for analysis of body instance. Restored automatically at
+ the end of the subprogram.
+ * gnat1drv.adb (Adjust_Global_Switches): Set
+ Check_Validity_Of_Parameters to False in GNATprove mode.
+ * opt.ads (Check_Validity_Of_Parameters): Document switch to
+ set option.
+
2017-09-08 Eric Botcazou <ebotcazou@adacore.com>
* sem_util.adb (NCT_Tables_In_Use): Move to library level from...
end case;
end Get_Binary_Nkind;
+ -----------------------
+ -- Get_Called_Entity --
+ -----------------------
+
+ function Get_Called_Entity (Call : Node_Id) return Entity_Id is
+ Nam : constant Node_Id := Name (Call);
+ Id : Entity_Id;
+
+ begin
+ if Nkind (Nam) = N_Explicit_Dereference then
+ Id := Etype (Nam);
+ pragma Assert (Ekind (Id) = E_Subprogram_Type);
+
+ elsif Nkind (Nam) = N_Selected_Component then
+ Id := Entity (Selector_Name (Nam));
+
+ elsif Nkind (Nam) = N_Indexed_Component then
+ Id := Entity (Selector_Name (Prefix (Nam)));
+
+ else
+ Id := Entity (Nam);
+ end if;
+
+ return Id;
+ end Get_Called_Entity;
+
-------------------
-- Get_Low_Bound --
-------------------
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2017, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- referencing this entity. It is an error to call this function if Ekind
-- (Op) /= E_Operator.
+ function Get_Called_Entity (Call : Node_Id) return Entity_Id;
+ -- Returns the entity associated with the call
+
function Get_Low_Bound (E : Entity_Id) return Node_Id;
- -- For an index subtype or string literal subtype, return its low bound
+ -- For an index subtype or string literal subtype, returns its low bound
function Get_Unary_Nkind (Op : Entity_Id) return Node_Kind;
-- Op must be an entity with an Ekind of E_Operator. This function returns
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
+ -- If the context of an instance is not subject to SPARK_Mode "off",
+ -- and the generic spec is subject to an explicit SPARK_Mode pragma,
+ -- the latter should be the one applicable to the instance.
+
+ if not Ignore_SPARK_Mode_Pragmas_In_Instance
+ and then Saved_SM /= Off
+ and then Present (SPARK_Pragma (Gen_Unit))
+ then
+ Set_SPARK_Mode (Gen_Unit);
+ end if;
+
Analyze_Instance_And_Renamings;
+ -- Restore SPARK_Mode from the context after analysis of the package
+ -- declaration, so that the SPARK_Mode on the generic spec does not
+ -- apply to the pending instance for the instance body.
+
+ if not Ignore_SPARK_Mode_Pragmas_In_Instance
+ and then Saved_SM /= Off
+ and then Present (SPARK_Pragma (Gen_Unit))
+ then
+ Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+ end if;
+
-- If the generic is marked Import (Intrinsic), then so is the
-- instance. This indicates that there is no body to instantiate. If
-- generic is marked inline, so it the instance, and the anonymous
Opt.Ada_Version_Pragma := Body_Info.Version_Pragma;
Restore_Warnings (Body_Info.Warnings);
- -- Install the SPARK mode which applies to the subprogram body
+ -- Install the SPARK mode which applies to the subprogram body from the
+ -- instantiation context. This may be refined further if an explicit
+ -- SPARK_Mode pragma applies to the generic body.
Install_SPARK_Mode (Body_Info.SPARK_Mode, Body_Info.SPARK_Mode_Pragma);
Ignore_SPARK_Mode_Pragmas_In_Instance := True;
end if;
+ -- If the context of an instance is not subject to SPARK_Mode "off",
+ -- and the generic body is subject to an explicit SPARK_Mode pragma,
+ -- the latter should be the one applicable to the instance.
+
+ if not Ignore_SPARK_Mode_Pragmas_In_Instance
+ and then SPARK_Mode /= Off
+ and then Present (SPARK_Pragma (Gen_Body_Id))
+ then
+ Set_SPARK_Mode (Gen_Body_Id);
+ end if;
+
Current_Sem_Unit := Body_Info.Current_Sem_Unit;
Create_Instantiation_Source
(Inst_Node,
-- second occurrence, the error is reported, and the tree traversal
-- is abandoned.
- function Get_Function_Id (Call : Node_Id) return Entity_Id;
- -- Return the entity associated with the function call
-
procedure Preanalyze_Without_Errors (N : Node_Id);
-- Preanalyze N without reporting errors. Very dubious, you can't just
-- go analyzing things more than once???
Formal : Node_Id;
begin
- Id := Get_Function_Id (Call);
+ Id := Get_Called_Entity (Call);
-- In case of previous error, no check is possible
Do_Traversal (N);
end Collect_Identifiers;
- ---------------------
- -- Get_Function_Id --
- ---------------------
-
- function Get_Function_Id (Call : Node_Id) return Entity_Id is
- Nam : constant Node_Id := Name (Call);
- Id : Entity_Id;
-
- begin
- if Nkind (Nam) = N_Explicit_Dereference then
- Id := Etype (Nam);
- pragma Assert (Ekind (Id) = E_Subprogram_Type);
-
- elsif Nkind (Nam) = N_Selected_Component then
- Id := Entity (Selector_Name (Nam));
-
- elsif Nkind (Nam) = N_Indexed_Component then
- Id := Entity (Selector_Name (Prefix (Nam)));
-
- else
- Id := Entity (Nam);
- end if;
-
- return Id;
- end Get_Function_Id;
-
-------------------------------
-- Preanalyze_Without_Errors --
-------------------------------
| N_Subprogram_Call
=>
declare
- Id : constant Entity_Id := Get_Function_Id (N);
+ Id : constant Entity_Id := Get_Called_Entity (N);
Formal : Node_Id;
Actual : Node_Id;
end if;
end Is_Volatile_Object;
+ -----------------------------
+ -- Iterate_Call_Parameters --
+ -----------------------------
+
+ procedure Iterate_Call_Parameters (Call : Node_Id) is
+ Formal : Entity_Id := First_Formal (Get_Called_Entity (Call));
+ Actual : Node_Id := First_Actual (Call);
+
+ begin
+ while Present (Formal) and then Present (Actual) loop
+ Handle_Parameter (Formal, Actual);
+ Formal := Next_Formal (Formal);
+ Actual := Next_Actual (Actual);
+ end loop;
+ end Iterate_Call_Parameters;
+
---------------------------
-- Itype_Has_Declaration --
---------------------------
-- for something actually declared as volatile, not for an object that gets
-- treated as volatile (see Einfo.Treat_As_Volatile).
+ generic
+ with procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id);
+ procedure Iterate_Call_Parameters (Call : Node_Id);
+ -- Calls Handle_Parameter for each pair of formal and actual parameters of
+ -- a function, procedure, or entry call.
+
function Itype_Has_Declaration (Id : Entity_Id) return Boolean;
-- Applies to Itypes. True if the Itype is attached to a declaration for
-- the type through its Parent field, which may or not be present in the
projects / gcc.git / commitdiff