+2014-05-21 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * freeze.adb (Freeze_Record_Type): Update the use of
+ Is_SPARK_Volatile.
+ * sem_ch3.adb (Analyze_Object_Contract): Update the use of
+ Is_SPARK_Volatile.
+ (Process_Discriminants): Update the use of Is_SPARK_Volatile.
+ * sem_ch5.adb (Analyze_Iterator_Specification): Update the use
+ of Is_SPARK_Volatile.
+ (Analyze_Loop_Parameter_Specification):
+ Update the use of Is_SPARK_Volatile.
+ * sem_ch6.adb (Process_Formals): Catch an illegal use of an IN
+ formal parameter when its type is volatile.
+ * sem_prag.adb (Analyze_Global_Item): Update the use of
+ Is_SPARK_Volatile.
+ * sem_res.adb (Resolve_Entity_Name): Correct the guard which
+ determines whether an entity is a volatile source SPARK object.
+ * sem_util.adb (Has_Enabled_Property): Accout for external
+ properties being set on objects other than abstract states
+ and variables. An example would be a formal parameter.
+ (Is_SPARK_Volatile): New routine.
+ (Is_SPARK_Volatile_Object):
+ Remove the entity-specific tests. Call routine Is_SPARK_Volatile
+ when checking entities and/or types.
+ * sem_util.ads (Is_SPARK_Volatile): New routine.
+
2014-05-21 Robert Dewar <dewar@adacore.com>
* sem_warn.adb: Minor fix to warning messages (use ?? instead
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
- if Is_SPARK_Volatile_Object (Rec) then
+ if Is_SPARK_Volatile (Rec) then
-- A discriminated type cannot be volatile (SPARK RM C.6(4))
Comp := First_Component (Rec);
while Present (Comp) loop
if Comes_From_Source (Comp)
- and then Is_SPARK_Volatile_Object (Comp)
+ and then Is_SPARK_Volatile (Comp)
then
Error_Msg_Name_1 := Chars (Rec);
Error_Msg_N
-- actuals in instantiations (SPARK RM 7.1.3(6)).
if SPARK_Mode = On
- and then Is_SPARK_Volatile_Object (Obj_Id)
+ and then Is_SPARK_Volatile (Obj_Id)
and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
then
Error_Msg_N ("constant cannot be volatile", Obj_Id);
-- they are not standard Ada legality rules.
if SPARK_Mode = On then
- if Is_SPARK_Volatile_Object (Obj_Id) then
+ if Is_SPARK_Volatile (Obj_Id) then
-- The declaration of a volatile object must appear at the
-- library level (SPARK RM 7.1.3(7), C.6(6)).
-- A non-volatile object cannot have volatile components
-- (SPARK RM 7.1.3(7)).
- if not Is_SPARK_Volatile_Object (Obj_Id)
+ if not Is_SPARK_Volatile (Obj_Id)
and then Has_Volatile_Component (Obj_Typ)
then
Error_Msg_N
-- (SPARK RM 7.1.3(6)).
if SPARK_Mode = On
- and then Is_SPARK_Volatile_Object (Defining_Identifier (Discr))
+ and then Is_SPARK_Volatile (Defining_Identifier (Discr))
then
Error_Msg_N ("discriminant cannot be volatile", Discr);
end if;
if SPARK_Mode = On
and then not Of_Present (N)
- and then Is_SPARK_Volatile_Object (Ent)
+ and then Is_SPARK_Volatile (Ent)
then
Error_Msg_N ("loop parameter cannot be volatile", Ent);
end if;
-- when SPARK_Mode is on as it is not a standard Ada legality check
-- (SPARK RM 7.1.3(6)).
- if SPARK_Mode = On and then Is_SPARK_Volatile_Object (Id) then
+ if SPARK_Mode = On and then Is_SPARK_Volatile (Id) then
Error_Msg_N ("loop parameter cannot be volatile", Id);
end if;
end Analyze_Loop_Parameter_Specification;
-- The following checks are relevant when SPARK_Mode is on as these
-- are not standard Ada legality rules.
- if SPARK_Mode = On
- and then Ekind_In (Scope (Formal), E_Function, E_Generic_Function)
- then
- -- A function cannot have a parameter of mode IN OUT or OUT
- -- (SPARK RM 6.1).
+ if SPARK_Mode = On then
+ if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then
- if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
- Error_Msg_N
- ("function cannot have parameter of mode `OUT` or `IN OUT`",
- Formal);
+ -- A function cannot have a parameter of mode IN OUT or OUT
+ -- (SPARK RM 6.1).
- -- A function cannot have a volatile formal parameter
- -- (SPARK RM 7.1.3(10)).
+ if Ekind_In (Formal, E_In_Out_Parameter, E_Out_Parameter) then
+ Error_Msg_N
+ ("function cannot have parameter of mode `OUT` or "
+ & "`IN OUT`", Formal);
- elsif Is_SPARK_Volatile_Object (Formal) then
+ -- A function cannot have a volatile formal parameter
+ -- (SPARK RM 7.1.3(10)).
+
+ elsif Is_SPARK_Volatile (Formal) then
+ Error_Msg_N
+ ("function cannot have a volatile formal parameter",
+ Formal);
+ end if;
+
+ -- A procedure cannot have a formal parameter of mode IN because
+ -- it behaves as a constant (SPARK RM 7.1.3(6)).
+
+ elsif Ekind (Scope (Formal)) = E_Procedure
+ and then Ekind (Formal) = E_In_Parameter
+ and then Is_SPARK_Volatile (Formal)
+ then
Error_Msg_N
- ("function cannot have a volatile formal parameter", Formal);
+ ("formal parameter of mode `IN` cannot be volatile", Formal);
end if;
end if;
-- SPARK_Mode is on as they are not standard Ada legality
-- rules.
- elsif SPARK_Mode = On
- and then Is_SPARK_Volatile_Object (Item_Id)
- then
+ elsif SPARK_Mode = On and then Is_SPARK_Volatile (Item_Id) then
+
-- A volatile object cannot appear as a global item of a
-- function (SPARK RM 7.1.3(9)).
-- standard Ada legality rules.
if SPARK_Mode = On
- and then Ekind_In (E, E_Abstract_State, E_Variable)
- and then Is_SPARK_Volatile_Object (E)
+ and then Is_Object (E)
+ and then Is_SPARK_Volatile (E)
+ and then Comes_From_Source (E)
and then
(Async_Writers_Enabled (E)
or else Effective_Reads_Enabled (E))
begin
-- A non-volatile object can never possess external properties
- if not Is_SPARK_Volatile_Object (Item_Id) then
+ if not Is_SPARK_Volatile (Item_Id) then
return False;
-- External properties related to variables come in two flavors -
-- Start of processing for Has_Enabled_Property
begin
+ -- Abstract states and variables have a flexible scheme of specifying
+ -- external properties.
+
if Ekind (Item_Id) = E_Abstract_State then
return State_Has_Enabled_Property;
- else pragma Assert (Ekind (Item_Id) = E_Variable);
+ elsif Ekind (Item_Id) = E_Variable then
return Variable_Has_Enabled_Property;
+
+ -- Otherwise a property is enabled when the related object is volatile
+
+ else
+ return Is_SPARK_Volatile (Item_Id);
end if;
end Has_Enabled_Property;
end if;
end Is_SPARK_Object_Reference;
+ -----------------------
+ -- Is_SPARK_Volatile --
+ -----------------------
+
+ function Is_SPARK_Volatile (Id : Entity_Id) return Boolean is
+ begin
+ return Is_Volatile (Id) or else Is_Volatile (Etype (Id));
+ end Is_SPARK_Volatile;
+
------------------------------
-- Is_SPARK_Volatile_Object --
------------------------------
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean is
begin
- if Nkind (N) = N_Defining_Identifier then
- return Is_Volatile (N) or else Is_Volatile (Etype (N));
-
- elsif Is_Entity_Name (N) then
- return
- Is_SPARK_Volatile_Object (Entity (N))
- or else Is_Volatile (Etype (N));
+ if Is_Entity_Name (N) then
+ return Is_SPARK_Volatile (Entity (N));
elsif Nkind (N) = N_Expanded_Name then
- return Is_SPARK_Volatile_Object (Entity (N));
+ return Is_SPARK_Volatile (Entity (N));
elsif Nkind (N) = N_Indexed_Component then
return Is_SPARK_Volatile_Object (Prefix (N));
function Is_SPARK_Object_Reference (N : Node_Id) return Boolean;
-- Determines if the tree referenced by N represents an object in SPARK
+ function Is_SPARK_Volatile (Id : Entity_Id) return Boolean;
+ -- This routine is similar to predicate Is_Volatile, but it takes SPARK
+ -- semantics into account. In SPARK volatile components to not render a
+ -- type volatile.
+
function Is_SPARK_Volatile_Object (N : Node_Id) return Boolean;
-- Determine whether an arbitrary node denotes a volatile object reference
-- according to the semantics of SPARK. To qualify as volatile, an object
- -- must be subject to aspect/pragma Volatile or Atomic or have a [sub]type
+ -- must be subject to aspect/pragma Volatile or Atomic, or have a [sub]type
-- subject to the same attributes. Note that volatile components do not
-- render an object volatile.
projects / thirdparty / gcc.git / commitdiff
