+2017-01-13 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_util.adb (Add_Inherited_Tagged_DIC):
+ Pass the object parameters of both the parent and the derived
+ type DIC procedure to the reference replacement circuitry.
+ (Find_DIC_Type): Modify the circuitry to present the partial
+ view of a private type in case the private type defines its own
+ DIC pragma.
+ (Replace_Object_And_Primitive_References): Add two
+ optional formal parameters. Update the comment on usage. Update
+ the replacement of references to object parameters.
+
+2017-01-13 Gary Dismukes <dismukes@adacore.com>
+
+ * einfo.adb, sem_ch6.adb, atree.adb: Minor reformatting and typo fix.
+
+2017-01-13 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_res.adb (Resolve_Actuals): Apply Scalar_Range_Check to
+ an out parameter that is a type conversion, independently of th
+ range check that may apply to the expression of the conversion,
+ for use in GNATProve.
+
+2017-01-13 Yannick Moy <moy@adacore.com>
+
+ * gnat1drv.adb (Gnat1drv): Move the implicit with for System in
+ GNATprove_Mode here to Frontend.
+ * frontend.adb (Frontend): Move the implicit with for System
+ in GNATprove_Mode here as it ismore correct this way; the old
+ place only worked by chance, since there were no overloaded names.
+ * rtsfind.ads (RE_Id, RE_Unit_Table): Add RE_Tasking_State.
+ * sem_attr.adb (Analyze_Attribute): In GNATprove_Mode, for the
+ four attributes identified in SRM 9(18), add an implicit with
+ to Ada.Task_Identification.
+ * sem_ch8.adb (Analyze_Subprogram_Renaming.Build_Class_Wide_Wrapper):
+ Deal specially with the wrapper introduced for AI05-0071 in GNATprove
+ mode.
+ * checks.adb (Apply_Discriminant_Check,
+ Apply_Selected_Length_Checks, Apply_Selected_Range_Checks):
+ In GNATprove mode, we do not apply the checks, but we still
+ analyze the expression to possibly issue errors on SPARK
+ code when a run-time error can be detected at compile time.
+ (Selected_Length_Checks, Selected_Range_Checks): Perform analysis
+ in GNATprove mode.
+
2017-01-13 Hristian Kirtchev <kirtchev@adacore.com>
* expander.adb (Expand): Add a warning about using return
-- information for the newly-allocated node is copied from it.
procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id);
- -- Fixup parent pointers for the syntactic children of Fix_Node after a
+ -- Fix up parent pointers for the syntactic children of Fix_Node after a
-- copy, setting them to Fix_Node when they pointed to Ref_Node.
procedure Mark_New_Ghost_Node (N : Node_Or_Entity_Id);
procedure Fix_Parents (Ref_Node, Fix_Node : Node_Id) is
procedure Fix_Parent (Field : Union_Id);
- -- Fixup one parent pointer. Field is checked to see if it points to
+ -- Fix up one parent pointer. Field is checked to see if it points to
-- a node, list, or element list that has a parent that points to
-- Ref_Node. If so, the parent is reset to point to Fix_Node.
T_Typ := Typ;
end if;
- -- Nothing to do if discriminant checks are suppressed or else no code
- -- is to be generated
-
- if not Expander_Active
- or else Discriminant_Checks_Suppressed (T_Typ)
- then
- return;
+ -- Only apply checks when generating code and discriminant checks are
+ -- not suppressed. In GNATprove mode, we do not apply the checks, but we
+ -- still analyze the expression to possibly issue errors on SPARK code
+ -- when a run-time error can be detected at compile time.
+
+ if not GNATprove_Mode then
+ if not Expander_Active
+ or else Discriminant_Checks_Suppressed (T_Typ)
+ then
+ return;
+ end if;
end if;
-- No discriminant checks necessary for an access when expression is
end;
end if;
+ -- In GNATprove mode, we do not apply the checks
+
+ if GNATprove_Mode then
+ return;
+ end if;
+
-- Here we need a discriminant check. First build the expression
-- for the comparisons of the discriminants:
or else (not Length_Checks_Suppressed (Target_Typ));
begin
+ -- Only apply checks when generating code. In GNATprove mode, we do
+ -- not apply the checks, but we still call Selected_Length_Checks to
+ -- possibly issue errors on SPARK code when a run-time error can be
+ -- detected at compile time.
+
-- Note: this means that we lose some useful warnings if the expander
- -- is not active, and we also lose these warnings in SPARK mode ???
+ -- is not active.
- if not Expander_Active then
+ if not Expander_Active and not GNATprove_Mode then
return;
end if;
R_Result :=
Selected_Length_Checks (Ck_Node, Target_Typ, Source_Typ, Empty);
+ if GNATprove_Mode then
+ return;
+ end if;
+
for J in 1 .. 2 loop
R_Cno := R_Result (J);
exit when No (R_Cno);
R_Result : Check_Result;
begin
- if not Expander_Active or not Checks_On then
- return;
+ -- Only apply checks when generating code. In GNATprove mode, we do not
+ -- apply the checks, but we still call Selected_Range_Checks to possibly
+ -- issue errors on SPARK code when a run-time error can be detected at
+ -- compile time.
+
+ if not GNATprove_Mode then
+ if not Expander_Active or not Checks_On then
+ return;
+ end if;
end if;
R_Result :=
Selected_Range_Checks (Ck_Node, Target_Typ, Source_Typ, Empty);
+ if GNATprove_Mode then
+ return;
+ end if;
+
for J in 1 .. 2 loop
R_Cno := R_Result (J);
exit when No (R_Cno);
-- Start of processing for Selected_Length_Checks
begin
- if not Expander_Active then
+ -- Checks will be applied only when generating code. In GNATprove mode,
+ -- we do not apply the checks, but we still call Selected_Length_Checks
+ -- to possibly issue errors on SPARK code when a run-time error can be
+ -- detected at compile time.
+
+ if not Expander_Active and not GNATprove_Mode then
return Ret_Result;
end if;
-- Start of processing for Selected_Range_Checks
begin
- if not Expander_Active then
+ -- Checks will be applied only when generating code. In GNATprove mode,
+ -- we do not apply the checks, but we still call Selected_Range_Checks
+ -- to possibly issue errors on SPARK code when a run-time error can be
+ -- detected at compile time.
+
+ if not Expander_Active and not GNATprove_Mode then
return Ret_Result;
end if;
function Is_Checked_Ghost_Entity (Id : E) return B is
begin
- -- Allow this attribute to appear on non-analyzed entities
+ -- Allow this attribute to appear on unanalyzed entities
pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
function Is_Ignored_Ghost_Entity (Id : E) return B is
begin
- -- Allow this attribute to appear on non-analyzed entities
+ -- Allow this attribute to appear on unanalyzed entities
pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is
begin
- -- Allow this attribute to appear on non-analyzed entities
+ -- Allow this attribute to appear on unanalyzed entities
pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is
begin
- -- Allow this attribute to appear on non-analyzed entities
+ -- Allow this attribute to appear on unanalyzed entities
pragma Assert (Nkind (Id) in N_Entity
or else Ekind (Id) = E_Void);
procedure Replace_Object_And_Primitive_References
(Expr : Node_Id;
Par_Typ : Entity_Id;
- Deriv_Typ : Entity_Id);
+ Deriv_Typ : Entity_Id;
+ Par_Obj : Entity_Id := Empty;
+ Deriv_Obj : Entity_Id := Empty);
-- Expr denotes an arbitrary expression. Par_Typ is a parent type in a
- -- type hierarchy. Deriv_Typ is a type derived from Par_Typ. Perform the
- -- following substitutions:
+ -- type hierarchy. Deriv_Typ is a type derived from Par_Typ. Par_Obj is
+ -- the formal parameter which emulates the current instance of Par_Typ.
+ -- Deriv_Obj is the formal parameter which emulates the current instance
+ -- of Deriv_Typ. Perform the following substitutions:
--
- -- * Replace a reference to the _object parameter of the parent type's
- -- DIC procedure with a reference to the _object parameter of the
- -- derived type's DIC procedure.
+ -- * Replace a reference to Par_Obj with a reference to Deriv_Obj if
+ -- applicable.
--
-- * Replace a call to an overridden parent primitive with a call to
-- the overriding derived type primitive.
Deriv_Typ : Entity_Id;
Stmts : in out List_Id)
is
- DIC_Args : constant List_Id :=
- Pragma_Argument_Associations (DIC_Prag);
- DIC_Arg : constant Node_Id := First (DIC_Args);
- DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg);
- Typ_Decl : constant Node_Id := Declaration_Node (Deriv_Typ);
+ Deriv_Decl : constant Node_Id := Declaration_Node (Deriv_Typ);
+ Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ);
+ DIC_Args : constant List_Id :=
+ Pragma_Argument_Associations (DIC_Prag);
+ DIC_Arg : constant Node_Id := First (DIC_Args);
+ DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg);
+ Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ);
Expr : Node_Id;
-- handled by the overriding/inheritance mechanism and do not require
-- an extra replacement pass.
+ pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc));
+
Replace_Object_And_Primitive_References
(Expr => Expr,
Par_Typ => Par_Typ,
- Deriv_Typ => Deriv_Typ);
+ Deriv_Typ => Deriv_Typ,
+ Par_Obj => First_Formal (Par_Proc),
+ Deriv_Obj => First_Formal (Deriv_Proc));
-- Preanalyze the DIC expression to detect errors and at the same
-- time capture the visibility of the proper package part.
- Set_Parent (Expr, Typ_Decl);
+ Set_Parent (Expr, Deriv_Decl);
Preanalyze_Assert_Expression (Expr, Any_Boolean);
-- Once the DIC assertion expression is fully processed, add a check
procedure Replace_Object_And_Primitive_References
(Expr : Node_Id;
Par_Typ : Entity_Id;
- Deriv_Typ : Entity_Id)
+ Deriv_Typ : Entity_Id;
+ Par_Obj : Entity_Id := Empty;
+ Deriv_Obj : Entity_Id := Empty)
is
- Deriv_Obj : Entity_Id;
- -- The _object parameter of the derived type's DIC procedure
-
- Par_Obj : Entity_Id;
- -- The _object parameter of the parent type's DIC procedure
-
function Replace_Ref (Ref : Node_Id) return Traverse_Result;
-- Substitute a reference to an entity with a reference to the
-- corresponding entity stored in in table Primitives_Mapping.
-- The reference mentions the _object parameter of the parent
-- type's DIC procedure.
- elsif Ref_Id = Par_Obj then
+ elsif Present (Par_Obj)
+ and then Present (Deriv_Obj)
+ and then Ref_Id = Par_Obj
+ then
New_Ref := New_Occurrence_Of (Deriv_Obj, Loc);
-- The reference to _object acts as an actual parameter in a
procedure Replace_Refs is new Traverse_Proc (Replace_Ref);
- -- Local variables
-
- Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ);
- Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ);
-
-- Start of processing for Replace_Object_And_Primitive_References
begin
- pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc));
-
- Deriv_Obj := First_Entity (Deriv_Proc);
- Par_Obj := First_Entity (Par_Proc);
-
-- Map each primitive operation of the parent type to the proper
-- primitive of the derived type.
function Find_DIC_Type (Typ : Entity_Id) return Entity_Id is
Curr_Typ : Entity_Id;
- DIC_Typ : Entity_Id;
+ -- The current type being examined in the parent hierarchy traversal
+
+ DIC_Typ : Entity_Id;
+ -- The type which carries the DIC pragma. This variable denotes the
+ -- partial view when private types are involved.
+
+ Par_Typ : Entity_Id;
+ -- The parent type of the current type. This variable denotes the full
+ -- view when private types are involved.
begin
-- The input type defines its own DIC pragma, therefore it is the owner
-- Look at the full view of a private type because the type may
-- have a hidden parent introduced in the full view.
- if Is_Private_Type (DIC_Typ)
- and then Present (Full_View (DIC_Typ))
+ Par_Typ := DIC_Typ;
+
+ if Is_Private_Type (Par_Typ)
+ and then Present (Full_View (Par_Typ))
then
- DIC_Typ := Full_View (DIC_Typ);
+ Par_Typ := Full_View (Par_Typ);
end if;
-- Stop the climb once the nearest parent type which defines a DIC
-- pragma of its own is encountered or when the root of the parent
-- chain is reached.
- exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = DIC_Typ;
+ exit when Has_Own_DIC (DIC_Typ) or else Curr_Typ = Par_Typ;
- Curr_Typ := DIC_Typ;
+ Curr_Typ := Par_Typ;
end loop;
end if;
end if;
end if;
+ -- In GNATprove mode, force loading of a few RTE units.
+
+ if GNATprove_Mode then
+ declare
+ Unused_E : Entity_Id;
+ begin
+ -- Ensure that System.Interrupt_Priority is available to
+ -- GNATprove for the generation of VCs related to ceiling
+ -- priority.
+ Unused_E := RTE (RE_Interrupt_Priority);
+ end;
+ end if;
+
-- Qualify all entity names in inner packages, package bodies, etc.
Exp_Dbug.Qualify_All_Entity_Names;
Original_Operating_Mode := Operating_Mode;
Frontend;
- -- In GNATprove mode, force loading of System unit to ensure that
- -- System.Interrupt_Priority is available to GNATprove for the
- -- generation of VCs related to ceiling priority.
-
- if GNATprove_Mode then
- declare
- Unused_E : constant Entity_Id :=
- Rtsfind.RTE (Rtsfind.RE_Interrupt_Priority);
- begin
- null;
- end;
- end if;
-
-- Exit with errors if the main source could not be parsed
if Sinput.Main_Source_File = No_Source_File then
RE_Abort_Task, -- Ada.Task_Identification
RE_Current_Task, -- Ada.Task_Identification
RO_AT_Task_Id, -- Ada.Task_Identification
+ RE_Tasking_State, -- Ada.Task_Identification
RE_Decimal_IO, -- Ada.Text_IO
RE_Fixed_IO, -- Ada.Text_IO
RE_Abort_Task => Ada_Task_Identification,
RE_Current_Task => Ada_Task_Identification,
RO_AT_Task_Id => Ada_Task_Identification,
+ RE_Tasking_State => Ada_Task_Identification,
RE_Decimal_IO => Ada_Text_IO,
RE_Fixed_IO => Ada_Text_IO,
end case;
+ -- In SPARK some attribute references depend on Tasking_State, so we
+ -- need to make sure we load this so that gnat2why has the entity
+ -- available. See SPARK RM 9(18) for the relevant rule.
+
+ if GNATprove_Mode then
+ declare
+ Unused : Entity_Id;
+ begin
+ case Attr_Id is
+ when Attribute_Callable |
+ Attribute_Caller |
+ Attribute_Count |
+ Attribute_Terminated =>
+ Unused := RTE (RE_Tasking_State);
+
+ when others =>
+ null;
+ end case;
+ end;
+ end if;
+
-- All errors raise Bad_Attribute, so that we get out before any further
-- damage occurs when an error is detected (for example, if we check for
-- one attribute expression, and the check succeeds, we want to be able
-- Start of processing for Fully_Conformant_Expressions
begin
- -- Non-conformant if paren count does not match. Note: if some idiot
+ -- Nonconformant if paren count does not match. Note: if some idiot
-- complains that we don't do this right for more than 3 levels of
-- parentheses, they will be treated with the respect they deserve.
return Entity (E1) = Entity (E2)
-- One may be a discriminant that has been replaced by
- -- the correspondding discriminal
+ -- the corresponding discriminal.
or else (Chars (Entity (E1)) = Chars (Entity (E2))
and then Ekind (Entity (E1)) = E_Discriminant
and then Ekind (Entity (E2)) = E_In_Parameter)
- -- AI12-050 : the loop variables of quantified expressions
- -- match if the have the same identifier, even though they
+ -- AI12-050 : The loop variables of quantified expressions
+ -- match if they have the same identifier, even though they
-- are different entities.
or else (Chars (Entity (E1)) = Chars (Entity (E2))
is
Loc : constant Source_Ptr := Sloc (N);
+ function Build_Expr_Fun_Call
+ (Subp_Id : Entity_Id;
+ Params : List_Id) return Node_Id;
+ -- Create a dispatching call to invoke function Subp_Id with actuals
+ -- built from the parameter specifications of list Params. Return
+ -- directly the call, so that it can be used inside an expression
+ -- function. This is a specificity of the GNATprove mode.
+
function Build_Call
(Subp_Id : Entity_Id;
Params : List_Id) return Node_Id;
end if;
end Build_Call;
+ -------------------------
+ -- Build_Expr_Fun_Call --
+ -------------------------
+
+ function Build_Expr_Fun_Call
+ (Subp_Id : Entity_Id;
+ Params : List_Id) return Node_Id
+ is
+ Actuals : constant List_Id := New_List;
+ Call_Ref : constant Node_Id := New_Occurrence_Of (Subp_Id, Loc);
+ Formal : Node_Id;
+
+ begin
+ -- Build the actual parameters of the call
+
+ Formal := First (Params);
+ while Present (Formal) loop
+ Append_To (Actuals,
+ Make_Identifier (Loc, Chars (Defining_Identifier (Formal))));
+ Next (Formal);
+ end loop;
+
+ -- Generate:
+ -- Subp_Id (Actuals);
+
+ pragma Assert (Ekind_In (Subp_Id, E_Function, E_Operator));
+
+ return Make_Function_Call (Loc,
+ Name => Call_Ref,
+ Parameter_Associations => Actuals);
+ end Build_Expr_Fun_Call;
+
----------------
-- Build_Spec --
----------------
Formal : Node_Id;
Prim_Op : Entity_Id;
Spec_Decl : Node_Id;
+ New_Spec : Node_Id;
-- Start of processing for Build_Class_Wide_Wrapper
-- Step 3: Create the declaration and the body of the wrapper, insert
-- all the pieces into the tree.
- Spec_Decl :=
- Make_Subprogram_Declaration (Loc,
- Specification => Build_Spec (Ren_Id));
- Insert_Before_And_Analyze (N, Spec_Decl);
+ -- In GNATprove mode, create a function wrapper in the form of an
+ -- expression function, so that an implicit postcondition relating
+ -- the result of calling the wrapper function and the result of the
+ -- dispatching call to the wrapped function is known during proof.
+
+ if GNATprove_Mode
+ and then Ekind_In (Ren_Id, E_Function, E_Operator)
+ then
+ New_Spec := Build_Spec (Ren_Id);
+ Body_Decl :=
+ Make_Expression_Function (Loc,
+ Specification => New_Spec,
+ Expression => Build_Expr_Fun_Call
+ (Subp_Id => Prim_Op,
+ Params => Parameter_Specifications (New_Spec)));
+
+ Wrap_Id := Defining_Entity (Body_Decl);
+
+ -- Otherwise, create separate spec and body for the subprogram
+
+ else
+ Spec_Decl :=
+ Make_Subprogram_Declaration (Loc,
+ Specification => Build_Spec (Ren_Id));
+ Insert_Before_And_Analyze (N, Spec_Decl);
+
+ Wrap_Id := Defining_Entity (Spec_Decl);
+
+ Body_Decl :=
+ Make_Subprogram_Body (Loc,
+ Specification => Build_Spec (Ren_Id),
+ Declarations => New_List,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Build_Call
+ (Subp_Id => Prim_Op,
+ Params =>
+ Parameter_Specifications
+ (Specification (Spec_Decl))))));
+
+ Set_Corresponding_Body (Spec_Decl, Defining_Entity (Body_Decl));
+ end if;
-- If the operator carries an Eliminated pragma, indicate that the
-- wrapper is also to be eliminated, to prevent spurious error when
-- using gnatelim on programs that include box-initialization of
-- equality operators.
- Wrap_Id := Defining_Entity (Spec_Decl);
Set_Is_Eliminated (Wrap_Id, Is_Eliminated (Prim_Op));
- Body_Decl :=
- Make_Subprogram_Body (Loc,
- Specification => Build_Spec (Ren_Id),
- Declarations => New_List,
- Handled_Statement_Sequence =>
- Make_Handled_Sequence_Of_Statements (Loc,
- Statements => New_List (
- Build_Call
- (Subp_Id => Prim_Op,
- Params =>
- Parameter_Specifications
- (Specification (Spec_Decl))))));
+ -- In GNATprove mode, insert the body in the tree for analysis
+
+ if GNATprove_Mode then
+ Insert_Before_And_Analyze (N, Body_Decl);
+ end if;
-- The generated body does not freeze and must be analyzed when the
-- class-wide wrapper is frozen. The body is only needed if expansion
if Ekind_In (F, E_Out_Parameter, E_In_Out_Parameter) then
- -- If there is a type conversion, to make sure the return value
+ -- If there is a type conversion, make sure the return value
-- meets the constraints of the variable before the conversion.
if Nkind (A) = N_Type_Conversion then
if Is_Scalar_Type (A_Typ) then
Apply_Scalar_Range_Check
(Expression (A), Etype (Expression (A)), A_Typ);
+
+ -- In addition, the returned value of the parameter
+ -- must satisfy the bounds of the object type (see
+ -- comment below).
+
+ Apply_Scalar_Range_Check (A, A_Typ, F_Typ);
+
else
Apply_Range_Check
(Expression (A), Etype (Expression (A)), A_Typ);
end if;
- -- If no conversion apply scalar range checks and length checks
- -- base on the subtype of the actual (NOT that of the formal).
+ -- If no conversion, apply scalar range checks and length check
+ -- based on the subtype of the actual (NOT that of the formal).
+ -- This indicates that the check takes place on return from the
+ -- call. During expansion the required constraint checks are
+ -- inserted. In GNATprove mode, in the absence of expansion,
+ -- the flag indicates that the returned value is valid.
else
if Is_Scalar_Type (F_Typ) then
Apply_Scalar_Range_Check (A, A_Typ, F_Typ);
+
elsif Is_Array_Type (F_Typ)
and then Ekind (F) = E_Out_Parameter
then
projects / thirdparty / gcc.git / commitdiff
