+2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_res.adb (Is_Protected_Operation_Call):
+ Add guards to account for a non-decorated selected component.
+
+2016-04-18 Yannick Moy <moy@adacore.com>
+
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): Improve
+ implementation of Body_Has_SPARK_Mode_On.
+ * sem_prag.adb, sem_prag.ads (Get_SPARK_Mode_From_Annotation):
+ New function replacing previous Get_SPARK_Mode_From_Pragma, that
+ deals also with aspects.
+ (Get_SPARK_Mode_Type): Make function internal again.
+ * inline.adb, sem_ch7.adb, sem_util.adb: Use new
+ Get_SPARK_Mode_From_Annotation.
+
2016-04-18 Hristian Kirtchev <kirtchev@adacore.com>
* contracts.adb (Analyze_Object_Contract): Update references to
elsif Present (Spec_Id)
and then
(No (SPARK_Pragma (Spec_Id))
- or else Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) /= On)
+ or else
+ Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) /= On)
then
return False;
Item := First (Aspect_Specifications (N));
while Present (Item) loop
if Get_Aspect_Id (Item) = Aspect_SPARK_Mode then
- return No (Expression (Item))
- or else
- (Nkind (Expression (Item)) = N_Identifier
- and then
- Get_SPARK_Mode_Type (Chars (Expression (Item))) = On);
+ return Get_SPARK_Mode_From_Annotation (Item) = On;
end if;
Next (Item);
if Present (Decls) then
Item := First (Decls);
while Present (Item) loop
- if Nkind (Item) = N_Pragma
- and then Get_Pragma_Id (Item) = Pragma_SPARK_Mode
- then
- return Get_SPARK_Mode_From_Pragma (Item) = On;
+
+ -- Pragmas that apply to a subprogram body are usually grouped
+ -- together. Look for a potential pragma SPARK_Mode among them.
+
+ if Nkind (Item) = N_Pragma then
+ if Get_Pragma_Id (Item) = Pragma_SPARK_Mode then
+ return Get_SPARK_Mode_From_Annotation (Item) = On;
+ end if;
+
+ -- Otherwise the first non-pragma declarative item terminates
+ -- the region where pragma SPARK_Mode may appear.
+
+ else
+ exit;
end if;
Next (Item);
end loop;
end if;
- -- Applicable SPARK_Mode is inherited from the enclosing subprogram
- -- or package.
+ -- Otherwise, the applicable SPARK_Mode is inherited from the
+ -- enclosing subprogram or package.
return SPARK_Mode = On;
end Body_Has_SPARK_Mode_On;
if Present (Spec_Id) and then Present (SPARK_Pragma (Body_Id)) then
if Present (SPARK_Pragma (Spec_Id)) then
- if Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Spec_Id)) = Off
+ if Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Spec_Id)) = Off
and then
- Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+ Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On
then
Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
Error_Msg_N ("incorrect application of SPARK_Mode#", N);
if Present (SPARK_Pragma (Body_Id)) then
if Present (SPARK_Aux_Pragma (Spec_Id)) then
- if Get_SPARK_Mode_From_Pragma (SPARK_Aux_Pragma (Spec_Id)) = Off
- and then
- Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+ if Get_SPARK_Mode_From_Annotation (SPARK_Aux_Pragma (Spec_Id)) =
+ Off
+ and then
+ Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Body_Id)) = On
then
Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
Error_Msg_N ("incorrect application of SPARK_Mode#", N);
-- original one, following the renaming chain) is returned. Otherwise the
-- entity is returned unchanged. Should be in Einfo???
+ function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
+ -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
+ -- Get_SPARK_Mode_From_Annotation. Convert a name into a corresponding
+ -- value of type SPARK_Mode_Type.
+
function Has_Extra_Parentheses (Clause : Node_Id) return Boolean;
-- Subsidiary to the analysis of pragmas Depends and Refined_Depends.
-- Determine whether dependency clause Clause is surrounded by extra
-- Issue an error if the new mode is less restrictive than
-- that of the context.
- if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
- and then Get_SPARK_Mode_From_Pragma (N) = On
+ if Get_SPARK_Mode_From_Annotation (Context_Pragma) = Off
+ and then Get_SPARK_Mode_From_Annotation (N) = On
then
Error_Msg_N
("cannot change SPARK_Mode from Off to On", Err_N);
-- Issue an error if the new mode is less restrictive
-- than that of the initial declaration.
- if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
- and then Get_SPARK_Mode_From_Pragma (N) = On
+ if Get_SPARK_Mode_From_Annotation (Entity_Pragma) = Off
+ and then Get_SPARK_Mode_From_Annotation (N) = On
then
Error_Msg_N ("incorrect use of SPARK_Mode", Err_N);
Error_Msg_Sloc := Sloc (Entity_Pragma);
end if;
end Get_SPARK_Mode_Type;
- --------------------------------
- -- Get_SPARK_Mode_From_Pragma --
- --------------------------------
+ ------------------------------------
+ -- Get_SPARK_Mode_From_Annotation --
+ ------------------------------------
- function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type is
- Args : List_Id;
+ function Get_SPARK_Mode_From_Annotation
+ (N : Node_Id) return SPARK_Mode_Type
+ is
Mode : Node_Id;
begin
- pragma Assert (Nkind (N) = N_Pragma);
- Args := Pragma_Argument_Associations (N);
+ if Nkind (N) = N_Aspect_Specification then
+ Mode := Expression (N);
- -- Extract the mode from the argument list
-
- if Present (Args) then
+ else pragma Assert (Nkind (N) = N_Pragma);
Mode := First (Pragma_Argument_Associations (N));
- return Get_SPARK_Mode_Type (Chars (Get_Pragma_Arg (Mode)));
- -- If SPARK_Mode pragma has no argument, default is ON
+ if Present (Mode) then
+ Mode := Get_Pragma_Arg (Mode);
+ end if;
+ end if;
+
+ -- Aspect or pragma SPARK_Mode specifies an explicit mode
+
+ if Present (Mode) then
+ if Nkind (Mode) = N_Identifier then
+ return Get_SPARK_Mode_Type (Chars (Mode));
+
+ -- In case of a malformed aspect or pragma, return the default None
+
+ else
+ return None;
+ end if;
+
+ -- Otherwise the lack of an expression defaults SPARK_Mode to On
else
return On;
end if;
- end Get_SPARK_Mode_From_Pragma;
+ end Get_SPARK_Mode_From_Annotation;
---------------------------
-- Has_Extra_Parentheses --
-- Context denotes the entity of the function, package or procedure where
-- Prag resides.
- function Get_SPARK_Mode_From_Pragma (N : Node_Id) return SPARK_Mode_Type;
- -- Given a pragma SPARK_Mode node, return corresponding mode id
-
- function Get_SPARK_Mode_Type (N : Name_Id) return SPARK_Mode_Type;
- -- Subsidiary to the analysis of pragma SPARK_Mode as well as subprogram
- -- Get_SPARK_Mode_From_Pragma. Convert a name into a corresponding value
- -- of type SPARK_Mode_Type.
+ function Get_SPARK_Mode_From_Annotation
+ (N : Node_Id) return SPARK_Mode_Type;
+ -- Given an aspect or pragma SPARK_Mode node, return corresponding mode id
procedure Initialize;
-- Initializes data structures used for pragma processing. Must be called
return
Pref = Obj_Ref
+ and then Present (Etype (Pref))
and then Is_Protected_Type (Etype (Pref))
and then Is_Entity_Name (Subp)
+ and then Present (Entity (Subp))
and then Ekind_In (Entity (Subp), E_Entry,
E_Entry_Family,
E_Function,
null;
elsif Present (SPARK_Pragma (Context)) then
- SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Context));
+ SPARK_Mode := Get_SPARK_Mode_From_Annotation (SPARK_Pragma (Context));
end if;
end Save_SPARK_Mode_And_Set;
projects / gcc.git / commitdiff