[Ada] Remove SPARK legality checks performed in GNATprove
Arnaud Charlet
charlet@adacore.com
Mon Apr 18 10:38:00 GMT 2016
Checks that some types and objects are fully default initialized should
be performed in GNATprove, where relevant information about SPARK status
of private types in particular is available. Move two tests performed in
the frontend to GNATprove here.
Tested on x86_64-pc-linux-gnu, committed on trunk
2016-04-18 Yannick Moy <moy@adacore.com>
* contracts.adb (Analyze_Object_Contract,
Analyze_Protected_Contract): Remove tests performed in GNATprove.
* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization):
Remove query for tests performed in GNATprove.
-------------- next part --------------
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 235116)
+++ sem_util.adb (working copy)
@@ -9046,110 +9046,6 @@
end if;
end Has_Enabled_Property;
- -------------------------------------
- -- Has_Full_Default_Initialization --
- -------------------------------------
-
- function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean is
- Arg : Node_Id;
- Comp : Entity_Id;
- Prag : Node_Id;
-
- begin
- -- A private type and its full view is fully default initialized when it
- -- is subject to pragma Default_Initial_Condition without an argument or
- -- with a non-null argument. Since any type may act as the full view of
- -- a private type, this check must be performed prior to the specialized
- -- tests below.
-
- if Has_Default_Init_Cond (Typ)
- or else Has_Inherited_Default_Init_Cond (Typ)
- then
- Prag := Get_Pragma (Typ, Pragma_Default_Initial_Condition);
-
- -- Pragma Default_Initial_Condition must be present if one of the
- -- related entity flags is set.
-
- pragma Assert (Present (Prag));
- Arg := First (Pragma_Argument_Associations (Prag));
-
- -- A non-null argument guarantees full default initialization
-
- if Present (Arg) then
- return Nkind (Arg) /= N_Null;
-
- -- Otherwise the missing argument defaults the pragma to "True" which
- -- is considered a non-null argument (see above).
-
- else
- return True;
- end if;
- end if;
-
- -- A scalar type is fully default initialized if it is subject to aspect
- -- Default_Value.
-
- if Is_Scalar_Type (Typ) then
- return Has_Default_Aspect (Typ);
-
- -- An array type is fully default initialized if its element type is
- -- scalar and the array type carries aspect Default_Component_Value or
- -- the element type is fully default initialized.
-
- elsif Is_Array_Type (Typ) then
- return
- Has_Default_Aspect (Typ)
- or else Has_Full_Default_Initialization (Component_Type (Typ));
-
- -- A protected type, record type or type extension is fully default
- -- initialized if all its components either carry an initialization
- -- expression or have a type that is fully default initialized. The
- -- parent type of a type extension must be fully default initialized.
-
- elsif Is_Record_Type (Typ) or else Is_Protected_Type (Typ) then
-
- -- Inspect all entities defined in the scope of the type, looking for
- -- uninitialized components.
-
- Comp := First_Entity (Typ);
- while Present (Comp) loop
- if Ekind (Comp) = E_Component
- and then Comes_From_Source (Comp)
- and then No (Expression (Parent (Comp)))
- and then not Has_Full_Default_Initialization (Etype (Comp))
- then
- return False;
- end if;
-
- Next_Entity (Comp);
- end loop;
-
- -- Ensure that the parent type of a type extension is fully default
- -- initialized.
-
- if Etype (Typ) /= Typ
- and then not Has_Full_Default_Initialization (Etype (Typ))
- then
- return False;
- end if;
-
- -- If we get here, then all components and parent portion are fully
- -- default initialized.
-
- return True;
-
- -- A task type is fully default initialized by default
-
- elsif Is_Task_Type (Typ) then
- return True;
-
- -- Otherwise the type is not fully default initialized
-
- else
- return False;
- end if;
- end Has_Full_Default_Initialization;
-
--------------------
-- Has_Infinities --
--------------------
Index: sem_util.ads
===================================================================
--- sem_util.ads (revision 235100)
+++ sem_util.ads (working copy)
@@ -1034,19 +1034,6 @@
-- Determine whether subprogram Subp_Id has an effectively volatile formal
-- parameter or returns an effectively volatile value.
- function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean;
- -- Determine whether type Typ defines "full default initialization" as
- -- specified by SPARK RM 3.1. To qualify as such, the type must be
- -- * A scalar type with specified Default_Value
- -- * An array-of-scalar type with specified Default_Component_Value
- -- * An array type whose element type defines full default initialization
- -- * A protected type, record type or type extension whose components
- -- either include a default expression or have a type which defines
- -- full default initialization. In the case of type extensions, the
- -- parent type defines full default initialization.
- -- * A task type
- -- * A private type whose Default_Initial_Condition is non-null
-
function Has_Infinities (E : Entity_Id) return Boolean;
-- Determines if the range of the floating-point type E includes
-- infinities. Returns False if E is not a floating-point type.
Index: contracts.adb
===================================================================
--- contracts.adb (revision 235115)
+++ contracts.adb (working copy)
@@ -660,7 +660,6 @@
Obj_Typ : constant Entity_Id := Etype (Obj_Id);
AR_Val : Boolean := False;
AW_Val : Boolean := False;
- Encap_Id : Entity_Id;
ER_Val : Boolean := False;
EW_Val : Boolean := False;
Items : Node_Id;
@@ -872,28 +871,6 @@
Obj_Id);
end if;
end if;
-
- -- A variable whose Part_Of pragma specifies a single concurrent
- -- type as encapsulator must be (SPARK RM 9.4):
- -- * Of a type that defines full default initialization, or
- -- * Declared with a default value, or
- -- * Imported
-
- Encap_Id := Encapsulating_State (Obj_Id);
-
- if Present (Encap_Id)
- and then Is_Single_Concurrent_Object (Encap_Id)
- and then not Has_Full_Default_Initialization (Etype (Obj_Id))
- and then not Has_Initial_Value (Obj_Id)
- and then not Is_Imported (Obj_Id)
- then
- Error_Msg_N ("& requires full default initialization", Obj_Id);
-
- Error_Msg_Name_1 := Chars (Encap_Id);
- Error_Msg_N
- (Fix_Msg (Encap_Id, "\object acts as constituent of single "
- & "protected type %"), Obj_Id);
- end if;
end if;
end if;
@@ -1137,7 +1114,6 @@
procedure Analyze_Protected_Contract (Prot_Id : Entity_Id) is
Items : constant Node_Id := Contract (Prot_Id);
- Mode : SPARK_Mode_Type;
begin
-- Do not analyze a contract multiple times
@@ -1149,30 +1125,6 @@
Set_Analyzed (Items);
end if;
end if;
-
- -- Due to the timing of contract analysis, delayed pragmas may be
- -- subject to the wrong SPARK_Mode, usually that of the enclosing
- -- context. To remedy this, restore the original SPARK_Mode of the
- -- related protected unit.
-
- Save_SPARK_Mode_And_Set (Prot_Id, Mode);
-
- -- A protected type must define full default initialization
- -- (SPARK RM 9.4). This check is relevant only when SPARK_Mode is on as
- -- it is not a standard Ada legality rule.
-
- if SPARK_Mode = On
- and then not Has_Full_Default_Initialization (Prot_Id)
- then
- Error_Msg_N
- ("protected type & must define full default initialization",
- Prot_Id);
- end if;
-
- -- Restore the SPARK_Mode of the enclosing context after all delayed
- -- pragmas have been analyzed.
-
- Restore_SPARK_Mode (Mode);
end Analyze_Protected_Contract;
-------------------------------------------
More information about the Gcc-patches
mailing list