+2014-01-29 Thomas Quinot <quinot@adacore.com>
+
+ * sem_ch4.adb (Find_Component_In_Instance): Update comment.
+
+2014-01-29 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_util.adb (Build_Task_Image_Prefix): Indicate that the
+ resulting string is an internal entity. and thus requires no
+ initialization. This is relevant when Initialize_ Scalars is
+ enabled, because the resultant spurious initialization may lead to
+ secondary stack anomalies that produce a mangled name for a task.
+
+2014-01-29 Yannick Moy <moy@adacore.com>
+
+ * sem_ch6.adb (Analyze_Subprogram_Body_Helper): SPARK_Mode
+ not inherited from spec anymore. Check consistency
+ rules after processing of declarations.
+ * sem_ch7.adb (Analyze_Package_Body_Helper): SPARK_Mode not inherited
+ from spec anymore. Check consistency rules after processing of
+ declarations.
+ (Analyze_Package_Declaration): Set SPARK_Mode only for non-generic
+ packages.
+ * sem_prag.adb (Analyze_Pragma/Pragma_SPARK_Mode): Implement new
+ consistency rules.
+
2014-01-27 Robert Dewar <dewar@adacore.com>
* sem_res.adb (Resolve_Comparison_Op): Add type name/location
Low_Bound => Make_Integer_Literal (Loc, 1),
High_Bound => New_Occurrence_Of (Len, Loc)))))));
+ -- Indicate that the result is an internal temporary, so it does not
+ -- receive a bogus initialization when declaration is expanded. This
+ -- is both efficient, and prevents anomalies in the handling of
+ -- dynamic objects on the secondary stack.
+
+ Set_Is_Internal (Res);
Pos := Make_Temporary (Loc, 'P');
Append_To (Decls,
-- In an instance, a component of a private extension may not be visible
-- while it was visible in the generic. Search candidate scope for a
-- component with the proper identifier. This is only done if all other
- -- searches have failed. When the match is found (it always will be),
- -- the Etype of both N and Sel are set from this component, and the
- -- entity of Sel is set to reference this component.
- -- ??? no longer true that a match is found ???
+ -- searches have failed. If a match is found, the Etype of both N and
+ -- Sel are set from this component, and the entity of Sel is set to
+ -- reference this component. If no match is found, Entity (Sel) remains
+ -- unset.
function Has_Mode_Conformant_Spec (Comp : Entity_Id) return Boolean;
-- It is known that the parent of N denotes a subprogram call. Comp
Push_Scope (Spec_Id);
- -- Set SPARK_Mode
+ -- Set SPARK_Mode from context
- -- For internally generated subprogram, always off. But generic
- -- instances are not generated implicitly, so are never considered
- -- as internal, even though Comes_From_Source is false.
-
- if not Comes_From_Source (Spec_Id)
- and then not Is_Generic_Instance (Spec_Id)
- then
- SPARK_Mode := Off;
- SPARK_Mode_Pragma := Empty;
-
- -- Inherited from spec
-
- elsif Present (SPARK_Pragma (Spec_Id))
- and then not SPARK_Pragma_Inherited (Spec_Id)
- then
- SPARK_Mode_Pragma := SPARK_Pragma (Spec_Id);
- SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
- Set_SPARK_Pragma (Body_Id, SPARK_Pragma (Spec_Id));
- Set_SPARK_Pragma_Inherited (Body_Id, True);
-
- -- Otherwise set from context
-
- else
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id, True);
- end if;
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
-- Make sure that the subprogram is immediately visible. For
-- child units that have no separate spec this is indispensable.
Push_Scope (Body_Id);
- -- Set SPARK_Mode from context or OFF for internal routine
+ -- Set SPARK_Mode from context
- if Comes_From_Source (Body_Id) then
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id, True);
- else
- Set_SPARK_Pragma (Body_Id, Empty);
- Set_SPARK_Pragma_Inherited (Body_Id, False);
- SPARK_Mode := Off;
- SPARK_Mode_Pragma := Empty;
- end if;
+ Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Body_Id, True);
end if;
-- For stubs and bodies with no previous spec, generate references to
Analyze_Declarations (Declarations (N));
+ -- After declarations have been analyzed, the body has been set
+ -- its final value of SPARK_Mode. Check that SPARK_Mode for body
+ -- is consistent with SPARK_Mode for spec.
+
+ 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
+ and then
+ Get_SPARK_Mode_From_Pragma (SPARK_Pragma (Body_Id)) = On
+ then
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Spec_Id));
+ Error_Msg_NE
+ ("\value Off was set for SPARK_Mode on & #", N, Spec_Id);
+ end if;
+
+ elsif Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Body_Stub then
+ null;
+
+ else
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (Spec_Id);
+ Error_Msg_NE
+ ("\no value was set for SPARK_Mode on & #", N, Spec_Id);
+ end if;
+ end if;
+
-- Check completion, and analyze the statements
Check_Completion;
Generate_Definition (Designator);
- -- Set SPARK mode, always off for internal routines, otherwise set
- -- from current context (may be overwritten later with explicit pragma)
+ -- Set SPARK mode from current context (may be overwritten later with
+ -- explicit pragma).
- if Comes_From_Source (Designator) then
- Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Designator, True);
- else
- Set_SPARK_Pragma (Designator, Empty);
- Set_SPARK_Pragma_Inherited (Designator, False);
- end if;
+ Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Designator, True);
if Debug_Flag_C then
Write_Str ("==> subprogram spec ");
Push_Scope (Spec_Id);
- -- Set SPARK_Mode from private part of spec if it has a SPARK pragma.
- -- Note that in the default case, SPARK_Aux_Pragma will be a copy of
- -- SPARK_Pragma in the spec, so this properly handles the case where
- -- there is no explicit SPARK_Pragma mode in the private part.
-
- if Present (SPARK_Pragma (Spec_Id)) then
- SPARK_Mode_Pragma := SPARK_Aux_Pragma (Spec_Id);
- SPARK_Mode := Get_SPARK_Mode_From_Pragma (SPARK_Mode_Pragma);
- Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Body_Id, True);
+ -- Set SPARK_Mode only for non-generic package
- -- Otherwise set from context
+ if Ekind (Spec_Id) = E_Package then
+ -- Set SPARK_Mode from context
- else
Set_SPARK_Pragma (Body_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Body_Id, True);
- end if;
- -- Set elaboration code SPARK mode the same for now
+ -- Set elaboration code SPARK mode the same for now
- Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
- Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+ Set_SPARK_Aux_Pragma (Body_Id, SPARK_Pragma (Body_Id));
+ Set_SPARK_Aux_Pragma_Inherited (Body_Id, True);
+ end if;
Set_Categorization_From_Pragmas (N);
Inspect_Deferred_Constant_Completion (Declarations (N));
end if;
+ -- After declarations have been analyzed, the body has been set
+ -- its final value of SPARK_Mode. Check that SPARK_Mode for body
+ -- is consistent with SPARK_Mode for spec.
+
+ 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
+ then
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (SPARK_Aux_Pragma (Spec_Id));
+ Error_Msg_NE ("\value Off was set for SPARK_Mode on & #",
+ N, Spec_Id);
+ end if;
+
+ else
+ Error_Msg_Sloc := Sloc (SPARK_Pragma (Body_Id));
+ Error_Msg_N ("incorrect application of SPARK_Mode#", N);
+ Error_Msg_Sloc := Sloc (Spec_Id);
+ Error_Msg_NE ("\no value was set for SPARK_Mode on & #",
+ N, Spec_Id);
+ end if;
+ end if;
+
-- Analyze_Declarations has caused freezing of all types. Now generate
-- bodies for RACW primitives and stream attributes, if any.
Set_Etype (Id, Standard_Void_Type);
Set_Contract (Id, Make_Contract (Sloc (Id)));
- -- Inherit spark mode from context for now
+ -- Set SPARK_Mode from context only for non-generic package
- Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
- Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
- Set_SPARK_Pragma_Inherited (Id, True);
- Set_SPARK_Aux_Pragma_Inherited (Id, True);
+ if Ekind (Id) = E_Package then
+ Set_SPARK_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Aux_Pragma (Id, SPARK_Mode_Pragma);
+ Set_SPARK_Pragma_Inherited (Id, True);
+ Set_SPARK_Aux_Pragma_Inherited (Id, True);
+ end if;
-- Analyze aspect specifications immediately, since we need to recognize
-- things like Pure early enough to diagnose violations during analysis.
Spec_Id : Entity_Id;
Stmt : Node_Id;
- procedure Check_Pragma_Conformance (Old_Pragma : Node_Id);
- -- Verify the monotonicity of SPARK modes between the new pragma
- -- N, and the old pragma, Old_Pragma, that was inherited. If
- -- Old_Pragma is Empty, the call has no effect, otherwise we
- -- verify that the new mode is less restrictive than the old mode.
- -- For example, if the old mode is ON, then the new mode can be
- -- anything. But if the old mode is OFF, then the only allowed
- -- new mode is also OFF.
+ procedure Check_Pragma_Conformance
+ (Context_Pragma : Node_Id;
+ Entity_Pragma : Node_Id;
+ Entity : Entity_Id);
+ -- If Context_Pragma is not Empty, verify that the new pragma N
+ -- is compatible with the pragma Context_Pragma that was inherited
+ -- from the context:
+ -- . if Context_Pragma is ON, then the new mode can be anything
+ -- . if Context_Pragma is OFF, then the only allowed new mode is
+ -- also OFF.
+ --
+ -- If Entity is not Empty, verify that the new pragma N is
+ -- compatible with Entity_Pragma, the SPARK_Mode previously set
+ -- for Entity (which may be Empty):
+ -- . if Entity_Pragma is ON, then the new mode can be anything
+ -- . if Entity_Pragma is OFF, then the only allowed new mode is
+ -- also OFF.
+ -- . if Entity_Pragma is Empty, we always issue an error, as this
+ -- corresponds to a case where a previous section of Entity
+ -- had no SPARK_Mode set.
procedure Check_Library_Level_Entity (E : Entity_Id);
-- Verify that pragma is applied to library-level entity E
-- Check_Pragma_Conformance --
------------------------------
- procedure Check_Pragma_Conformance (Old_Pragma : Node_Id) is
+ procedure Check_Pragma_Conformance
+ (Context_Pragma : Node_Id;
+ Entity_Pragma : Node_Id;
+ Entity : Entity_Id) is
begin
- if Present (Old_Pragma) then
- pragma Assert (Nkind (Old_Pragma) = N_Pragma);
+ if Present (Context_Pragma) then
+ pragma Assert (Nkind (Context_Pragma) = N_Pragma);
-- New mode less restrictive than the established mode
- if Get_SPARK_Mode_From_Pragma (Old_Pragma) = Off
+ if Get_SPARK_Mode_From_Pragma (Context_Pragma) = Off
and then Mode_Id = On
then
Error_Msg_N
- ("cannot change 'S'P'A'R'K_Mode from Off to On", Arg1);
+ ("cannot change SPARK_Mode from Off to On", Arg1);
Error_Msg_Sloc := Sloc (SPARK_Mode_Pragma);
- Error_Msg_N ("\'S'P'A'R'K_Mode was set to Off#", Arg1);
+ Error_Msg_N ("\SPARK_Mode was set to Off#", Arg1);
+ raise Pragma_Exit;
+ end if;
+ end if;
+
+ if Present (Entity) then
+ if Present (Entity_Pragma) then
+ if Get_SPARK_Mode_From_Pragma (Entity_Pragma) = Off
+ and then Mode_Id = On
+ then
+ Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
+ Error_Msg_Sloc := Sloc (Entity_Pragma);
+ Error_Msg_NE
+ ("\value Off was set for SPARK_Mode on & #",
+ Arg1, Entity);
+ raise Pragma_Exit;
+ end if;
+ else
+ Error_Msg_N ("incorrect use of SPARK_Mode", Arg1);
+ Error_Msg_Sloc := Sloc (Entity);
+ Error_Msg_NE ("\no value was set for SPARK_Mode on & #",
+ Arg1, Entity);
raise Pragma_Exit;
end if;
end if;
then
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
Set_SPARK_Pragma (Spec_Id, N);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
then
Spec_Id := Defining_Entity (Stmt);
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
Set_SPARK_Pragma (Spec_Id, N);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
if List_Containing (N) = Private_Declarations (Context) then
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Aux_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity_Pragma => SPARK_Pragma (Spec_Id),
+ Entity => Spec_Id);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
else
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
then
Spec_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Spec_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Spec_Id));
-
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Spec_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
Set_SPARK_Pragma (Spec_Id, N);
Set_SPARK_Pragma_Inherited (Spec_Id, False);
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity_Pragma => SPARK_Aux_Pragma (Spec_Id),
+ Entity => Spec_Id);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
Context := Specification (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance (SPARK_Pragma (Body_Id));
+
+ if Present (Spec_Id) then
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity_Pragma => SPARK_Pragma (Spec_Id),
+ Entity => Spec_Id);
+ else
+ Check_Pragma_Conformance
+ (Context_Pragma => SPARK_Pragma (Body_Id),
+ Entity_Pragma => Empty,
+ Entity => Empty);
+ end if;
+
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
Spec_Id := Corresponding_Spec (Context);
Body_Id := Defining_Entity (Context);
Check_Library_Level_Entity (Body_Id);
- Check_Pragma_Conformance (SPARK_Aux_Pragma (Body_Id));
+ Check_Pragma_Conformance
+ (Context_Pragma => Empty,
+ Entity_Pragma => SPARK_Pragma (Body_Id),
+ Entity => Body_Id);
SPARK_Mode_Pragma := N;
SPARK_Mode := Mode_Id;
projects / thirdparty / gcc.git / commitdiff
