+2014-07-30 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch4.adb (Analyze_If_Expression): Resolve condition before
+ analyzing branches.
+ * sem_eval.adb (Out_Of_Range): Check for statically unevaluated
+ expression case.
+
+2014-07-30 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch13.adb (Analyze_Aspect, predicate cases): Diagnose use
+ of predicate aspect on entity other than a type.
+
+2014-07-30 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch6.adb (Body_Has_Contract): New predicate to determine
+ when a subprogram body without a previous spec cannot be inlined
+ in GNATprove mode, because it includes aspects or pragmas that
+ generate a SPARK contract clause.
+ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): A subprogram
+ instance cannot be inlined.
+
2014-07-30 Robert Dewar <dewar@adacore.com>
* debug.adb: Document that d7 suppresses compilation time output.
function Has_Some_Contract (Id : Entity_Id) return Boolean is
Items : constant Node_Id := Contract (Id);
+
begin
return Present (Items)
and then (Present (Pre_Post_Conditions (Items))
- or else
- Present (Contract_Test_Cases (Items))
- or else
- Present (Classifications (Items)));
+ or else Present (Contract_Test_Cases (Items))
+ or else Present (Classifications (Items)));
end Has_Some_Contract;
--------------------------
then
return False;
+ elsif Is_Generic_Instance (Spec_Id) then
+ return False;
+
-- Only inline subprograms whose body is marked SPARK_Mode On
elsif No (SPARK_Pragma (Body_Id))
Aspect_Predicate |
Aspect_Static_Predicate =>
+ -- These aspects apply only to subtypes
+
+ if not Is_Type (E) then
+ Error_Msg_N
+ ("predicate can only be specified for a subtype",
+ Aspect);
+ goto Continue;
+ end if;
+
-- Construct the pragma (always a pragma Predicate, with
-- flags recording whether it is static/dynamic). We also
-- set flags recording this in the type itself.
Check_Compiler_Unit ("if expression", N);
end if;
+ -- Analyze and resolve the condition. We need to resolve this now so
+ -- that it gets folded to True/False if possible, before we analyze
+ -- the THEN/ELSE branches, because when analyzing these branches, we
+ -- may call Is_Statically_Unevaluated, which expects the condition of
+ -- an enclosing IF to have been analyze/resolved/evaluated.
+
Analyze_Expression (Condition);
+ Resolve (Condition, Any_Boolean);
+
+ -- Analyze THEN expression and (if present) ELSE expression. For those
+ -- we delay resolution in the normal manner, because of overloading etc.
+
Analyze_Expression (Then_Expr);
if Present (Else_Expr) then
-- Analyze the aspect specifications of a subprogram body [stub]. It is
-- assumed that N has aspects.
+ function Body_Has_Contract return Boolean;
+ -- Check whether unanalyzed body has an aspect or pragma that may
+ -- generate a SPARK contrac.
+
procedure Check_Anonymous_Return;
-- Ada 2005: if a function returns an access type that denotes a task,
-- or a type that contains tasks, we must create a master entity for
end if;
end Analyze_Aspects_On_Body_Or_Stub;
+ -----------------------
+ -- Body_Has_Contract --
+ -----------------------
+
+ function Body_Has_Contract return Boolean is
+ Decls : constant List_Id := Declarations (N);
+ A_Spec : Node_Id;
+ A : Aspect_Id;
+ Decl : Node_Id;
+ P_Id : Pragma_Id;
+
+ begin
+ -- Check for unanalyzed aspects in the body that will
+ -- generate a contract.
+
+ if Present (Aspect_Specifications (N)) then
+ A_Spec := First (Aspect_Specifications (N));
+ while Present (A_Spec) loop
+ A := Get_Aspect_Id (Chars (Identifier (A_Spec)));
+
+ if A = Aspect_Contract_Cases
+ or else A = Aspect_Depends
+ or else A = Aspect_Global
+ or else A = Aspect_Pre
+ or else A = Aspect_Precondition
+ or else A = Aspect_Post
+ or else A = Aspect_Postcondition
+ then
+ return True;
+ end if;
+
+ Next (A_Spec);
+ end loop;
+ end if;
+
+ -- Check for pragmas that may generate a contract.
+
+ if Present (Decls) then
+ Decl := First (Decls);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Pragma then
+ P_Id := Get_Pragma_Id (Pragma_Name (Decl));
+
+ if P_Id = Pragma_Contract_Cases
+ or else P_Id = Pragma_Depends
+ or else P_Id = Pragma_Global
+ or else P_Id = Pragma_Pre
+ or else P_Id = Pragma_Precondition
+ or else P_Id = Pragma_Post
+ or else P_Id = Pragma_Postcondition
+ then
+ return True;
+ end if;
+ end if;
+
+ Next (Decl);
+ end loop;
+ end if;
+
+ return False;
+ end Body_Has_Contract;
+
----------------------------
-- Check_Anonymous_Return --
----------------------------
and then Full_Analysis
and then Comes_From_Source (Body_Id)
and then Is_List_Member (N)
+ and then not Body_Has_Contract
then
declare
Body_Spec : constant Node_Id :=
and then
Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
+ and then not Body_Has_Contract
then
Build_Body_To_Inline (N, Spec_Id);
end if;
and then Present (Spec_Id)
and then Nkind (Parent (Parent (Spec_Id))) = N_Subprogram_Declaration
and then Can_Be_Inlined_In_GNATprove_Mode (Spec_Id, Body_Id)
+ and then not Body_Has_Contract
then
Check_And_Build_Body_To_Inline (N, Spec_Id, Body_Id);
end if;
-- If we have the static expression case, then this is an illegality
-- in Ada 95 mode, except that in an instance, we never generate an
-- error (if the error is legitimate, it was already diagnosed in the
- -- template). The expression to compute the length of a packed array is
- -- attached to the array type itself, and deserves a separate message.
+ -- template).
if Is_Static_Expression (N)
and then not In_Instance
and then not In_Inlined_Body
and then Ada_Version >= Ada_95
then
- if Nkind (Parent (N)) = N_Defining_Identifier
+ -- No message if we are staticallly unevaluated
+
+ if Is_Statically_Unevaluated (N) then
+ null;
+
+ -- The expression to compute the length of a packed array is attached
+ -- to the array type itself, and deserves a separate message.
+
+ elsif Nkind (Parent (N)) = N_Defining_Identifier
and then Is_Array_Type (Parent (N))
and then Present (Packed_Array_Impl_Type (Parent (N)))
and then Present (First_Rep_Item (Parent (N)))
First_Rep_Item (Parent (N)));
Rewrite (N, Make_Integer_Literal (Sloc (N), Uint_1));
+ -- All cases except the special array case
+
else
Apply_Compile_Time_Constraint_Error
(N, "value not in range of}", CE_Range_Check_Failed);
projects / gcc.git / commitdiff