- -----------------------------
- -- Analyze_Object_Contract --
- -----------------------------
-
- procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
- Obj_Typ : constant Entity_Id := Etype (Obj_Id);
- AR_Val : Boolean := False;
- AW_Val : Boolean := False;
- ER_Val : Boolean := False;
- EW_Val : Boolean := False;
- Prag : Node_Id;
- Seen : Boolean := False;
-
- begin
- -- The loop parameter in an element iterator over a formal container
- -- is declared with an object declaration but no contracts apply.
-
- if Ekind (Obj_Id) = E_Loop_Parameter then
- return;
- end if;
-
- -- Constant related checks
-
- if Ekind (Obj_Id) = E_Constant then
-
- -- A constant cannot be effectively volatile. This check is only
- -- relevant with SPARK_Mode on as it is not a standard Ada legality
- -- rule. Do not flag internally-generated constants that map generic
- -- formals to actuals in instantiations (SPARK RM 7.1.3(6)).
-
- if SPARK_Mode = On
- and then Is_Effectively_Volatile (Obj_Id)
- and then No (Corresponding_Generic_Association (Parent (Obj_Id)))
-
- -- Don't give this for internally generated entities (such as the
- -- FIRST and LAST temporaries generated for bounds).
-
- and then Comes_From_Source (Obj_Id)
- then
- Error_Msg_N ("constant cannot be volatile", Obj_Id);
- end if;
-
- -- Variable related checks
-
- else pragma Assert (Ekind (Obj_Id) = E_Variable);
-
- -- The following checks are only relevant when SPARK_Mode is on as
- -- they are not standard Ada legality rules. Internally generated
- -- temporaries are ignored.
-
- if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then
- if Is_Effectively_Volatile (Obj_Id) then
-
- -- The declaration of an effectively volatile object must
- -- appear at the library level (SPARK RM 7.1.3(7), C.6(6)).
-
- if not Is_Library_Level_Entity (Obj_Id) then
- Error_Msg_N
- ("volatile variable & must be declared at library level",
- Obj_Id);
-
- -- An object of a discriminated type cannot be effectively
- -- volatile (SPARK RM C.6(4)).
-
- elsif Has_Discriminants (Obj_Typ) then
- Error_Msg_N
- ("discriminated object & cannot be volatile", Obj_Id);
-
- -- An object of a tagged type cannot be effectively volatile
- -- (SPARK RM C.6(5)).
-
- elsif Is_Tagged_Type (Obj_Typ) then
- Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
- end if;
-
- -- The object is not effectively volatile
-
- else
- -- A non-effectively volatile object cannot have effectively
- -- volatile components (SPARK RM 7.1.3(7)).
-
- if not Is_Effectively_Volatile (Obj_Id)
- and then Has_Volatile_Component (Obj_Typ)
- then
- Error_Msg_N
- ("non-volatile object & cannot have volatile components",
- Obj_Id);
- end if;
- end if;
- end if;
-
- if Is_Ghost_Entity (Obj_Id) then
-
- -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
-
- if Is_Effectively_Volatile (Obj_Id) then
- Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
-
- -- A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
-
- elsif Is_Imported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
-
- elsif Is_Exported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
- end if;
- end if;
-
- -- Analyze all external properties
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AR_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, AW_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, ER_Val);
- Seen := True;
- end if;
-
- Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes);
-
- if Present (Prag) then
- Analyze_External_Property_In_Decl_Part (Prag, EW_Val);
- Seen := True;
- end if;
-
- -- Verify the mutual interaction of the various external properties
-
- if Seen then
- Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val);
- end if;
- end if;
-
- -- Check whether the lack of indicator Part_Of agrees with the placement
- -- of the object with respect to the state space.
-
- Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
-
- if No (Prag) then
- Check_Missing_Part_Of (Obj_Id);
- end if;
-
- -- A ghost object cannot be imported or exported (SPARK RM 6.9(8))
-
- if Is_Ghost_Entity (Obj_Id) then
- if Is_Exported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
-
- elsif Is_Imported (Obj_Id) then
- Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
- end if;
- end if;
- end Analyze_Object_Contract;
-