+2017-01-12 Yannick Moy <moy@adacore.com>
+
+ * exp_spark.adb (Expand_SPARK_Potential_Renaming): Fix sloc of copied
+ subtree.
+
+2017-01-12 Justin Squirek <squirek@adacore.com>
+
+ * exp_attr.adb (Expand_N_Attribute_Reference):
+ Fix Finalization_Size case by properly resolving the type after
+ rewritting the node.
+
+2017-01-12 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * exp_util.adb (Build_DIC_Procedure_Body): Semi-insert the body into
+ the tree.
+ (Build_DIC_Procedure_Declaration): Semi-insert the body into the tree.
+ * binde.adb, exp_ch5.adb, sem_type.adb, sem.ads, sem_res.adb,
+ exp_sel.ads: Minor reformatting.
+
+2017-01-12 Justin Squirek <squirek@adacore.com>
+
+ * exp_ch6.adb (Expand_Call): Add guard to prevent
+ invariant checks from being created for internally generated
+ subprograms.
+
+2017-01-12 Bob Duff <duff@adacore.com>
+
+ * lib-writ.ads: Remove incorrect comment.
+
+2017-01-12 Javier Miranda <miranda@adacore.com>
+
+ * debug.adb (-gnatd.K): Enable generation of contract-only
+ procedures in CodePeer mode.
+ * contracts.adb (Build_And_Analyze_Contract_Only_Subprograms):
+ New subprogram.
+ (Analyze_Contracts): Generate contract-only procedures if -gnatdK is
+ set.
+ * scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): New
+ subprogram.
+ (Get_Contract_Only_Missing_Body_Name): New subprogram.
+ (Get_Contract_Only_Body): New subprogram.
+ (Set_Contract_Only_Body): New subprogram.
+ (Is_Contract_Only_Body): New subprogram.
+ (Set_Is_Contract_Only_Body): New subprogram.
+ (SCIL_Nodes): Replace table by hash-table.
+
2017-01-12 Hristian Kirtchev <kirtchev@adacore.com>
* exp_ch6.adb: Minor reformatting.
-- There is a lot of fiddly string manipulation below, because we don't
-- want to depend on misc utility packages like Ada.Characters.Handling.
- function Read_File (Name : String) return String_Ptr;
- -- Read the entire contents of the named file
-
function Get_Line return String;
-- Read the next line from the file content read by Read_File. Strip
-- leading and trailing blanks. Convert "(spec)" or "(body)" to
-- "%s"/"%b". Remove comments (Ada style; "--" to end of line).
+ function Read_File (Name : String) return String_Ptr;
+ -- Read the entire contents of the named file
+
+ ---------------
+ -- Read_File --
+ ---------------
+
function Read_File (Name : String) return String_Ptr is
-- All of the following calls should succeed, because we checked the
-- file in Switch.B, but we double check and raise Program_Error on
end if;
declare
- Len : constant Natural := Natural (File_Length (F));
- Result : constant String_Ptr := new String (1 .. Len);
- Len_Read : constant Natural := Read (F, Result (1)'Address, Len);
+ Len : constant Natural := Natural (File_Length (F));
+ Result : constant String_Ptr := new String (1 .. Len);
+ Len_Read : constant Natural :=
+ Read (F, Result (1)'Address, Len);
+
Status : Boolean;
begin
end;
end Read_File;
- S : String_Ptr := Read_File (Force_Elab_Order_File.all);
- Cur : Positive := 1;
+ Cur : Positive := 1;
+ S : String_Ptr := Read_File (Force_Elab_Order_File.all);
+
+ --------------
+ -- Get_Line --
+ --------------
function Get_Line return String is
First : Positive := Cur;
- Last : Natural;
+ Last : Natural;
+
begin
-- Skip to end of line
-- again.
declare
+ Body_String : constant String := "(body)";
+ BL : constant Positive := Body_String'Length;
+ Spec_String : constant String := "(spec)";
+ SL : constant Positive := Spec_String'Length;
+
Line : String renames S (First .. Last);
- Spec_String : constant String := "(spec)";
- SL : constant Positive := Spec_String'Length;
- Body_String : constant String := "(body)";
- BL : constant Positive := Body_String'Length;
- Is_Spec, Is_Body : Boolean := False;
+
+ Is_Body : Boolean := False;
+ Is_Spec : Boolean := False;
+
begin
if Line'Length >= SL
and then Line (Last - SL + 1 .. Last) = Spec_String
end;
end Get_Line;
+ -- Local variables
+
Empty_Name : constant Unit_Name_Type := Name_Find ("");
- Prev_Unit : Unit_Id := No_Unit_Id;
+ Prev_Unit : Unit_Id := No_Unit_Id;
+
+ -- Start of processing for Force_Elab_Order
begin
-- Loop through the file content, and build a dependency link for each
with Aspects; use Aspects;
with Atree; use Atree;
+with Debug; use Debug;
with Einfo; use Einfo;
with Elists; use Elists;
with Errout; use Errout;
with Sinfo; use Sinfo;
with Snames; use Snames;
with Stringt; use Stringt;
+with SCIL_LL; use SCIL_LL;
with Tbuild; use Tbuild;
package body Contracts is
+ procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id);
+ -- (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
+ -- contract-only subprogram body of eligible subprograms found in L, adds
+ -- them to their corresponding list of declarations, and analyzes them.
+
procedure Analyze_Contracts
(L : List_Id;
Freeze_Nod : Node_Id;
procedure Analyze_Contracts (L : List_Id) is
begin
+ if CodePeer_Mode and then Debug_Flag_Dot_KK then
+ Build_And_Analyze_Contract_Only_Subprograms (L);
+ end if;
+
Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty);
end Analyze_Contracts;
(Obj_Id => Defining_Entity (Decl),
Freeze_Id => Freeze_Id);
- -- Protected untis
+ -- Protected units
elsif Nkind_In (Decl, N_Protected_Type_Declaration,
N_Single_Protected_Declaration)
Pop_Scope;
end Save_Global_References_In_Contract;
+ -------------------------------------------------
+ -- Build_And_Analyze_Contract_Only_Subprograms --
+ -------------------------------------------------
+
+ procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is
+ procedure Analyze_Contract_Only_Subprograms (L : List_Id);
+ -- Analyze the contract-only subprograms of L
+
+ procedure Append_Contract_Only_Subprograms (Subp_List : List_Id);
+ -- Append the contract-only bodies of Subp_List to its declarations list
+
+ function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id;
+ -- If E is an entity for a non-imported subprogram specification with
+ -- pre/postconditions and we are compiling with CodePeer mode, then this
+ -- procedure will create a wrapper to help Gnat2scil process its
+ -- contracts. Return Empty if the wrapper cannot be built.
+
+ function Build_Contract_Only_Subprograms (L : List_Id) return List_Id;
+ -- Build the contract-only subprograms of all eligible subprograms found
+ -- in list L.
+
+ function Has_Private_Declarations (N : Node_Id) return Boolean;
+ -- Return True for package specs, task definitions, and protected type
+ -- definitions whose list of private declarations is not empty.
+
+ ---------------------------------------
+ -- Analyze_Contract_Only_Subprograms --
+ ---------------------------------------
+
+ procedure Analyze_Contract_Only_Subprograms (L : List_Id) is
+ procedure Analyze_Contract_Only_Bodies;
+ -- Analyze all the contract-only bodies of L
+
+ ----------------------------------
+ -- Analyze_Contract_Only_Bodies --
+ ----------------------------------
+
+ procedure Analyze_Contract_Only_Bodies is
+ Decl : Node_Id;
+
+ begin
+ Decl := First (L);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Subprogram_Body
+ and then Is_Contract_Only_Body
+ (Defining_Unit_Name (Specification (Decl)))
+ then
+ Analyze (Decl);
+ end if;
+
+ Next (Decl);
+ end loop;
+ end Analyze_Contract_Only_Bodies;
+
+ -- Start of processing for Analyze_Contract_Only_Subprograms
+
+ begin
+ if Ekind (Current_Scope) /= E_Package then
+ Analyze_Contract_Only_Bodies;
+
+ else
+ declare
+ Pkg_Spec : constant Node_Id :=
+ Package_Specification (Current_Scope);
+
+ begin
+ if not Has_Private_Declarations (Pkg_Spec) then
+ Analyze_Contract_Only_Bodies;
+
+ -- For packages with private declarations, the contract-only
+ -- bodies of subprograms defined in the visible part of the
+ -- package are added to its private declarations (to ensure
+ -- that they do not cause premature freezing of types and also
+ -- that they are analyzed with proper visibility). Hence they
+ -- will be analyzed later.
+
+ elsif Visible_Declarations (Pkg_Spec) = L then
+ null;
+
+ elsif Private_Declarations (Pkg_Spec) = L then
+ Analyze_Contract_Only_Bodies;
+ end if;
+ end;
+ end if;
+ end Analyze_Contract_Only_Subprograms;
+
+ --------------------------------------
+ -- Append_Contract_Only_Subprograms --
+ --------------------------------------
+
+ procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is
+ begin
+ if No (Subp_List) then
+ return;
+ end if;
+
+ if Ekind (Current_Scope) /= E_Package then
+ Append_List (Subp_List, To => L);
+
+ else
+ declare
+ Pkg_Spec : constant Node_Id :=
+ Package_Specification (Current_Scope);
+
+ begin
+ if not Has_Private_Declarations (Pkg_Spec) then
+ Append_List (Subp_List, To => L);
+
+ -- If the package has private declarations then append them to
+ -- its private declarations; they will be analyzed when the
+ -- contracts of its private declarations are analyzed.
+
+ else
+ Append_List
+ (List => Subp_List,
+ To => Private_Declarations (Pkg_Spec));
+ end if;
+ end;
+ end if;
+ end Append_Contract_Only_Subprograms;
+
+ ------------------------------------
+ -- Build_Contract_Only_Subprogram --
+ ------------------------------------
+
+ -- This procedure takes care of building a wrapper to generate better
+ -- analysis results in the case of a call to a subprogram whose body
+ -- is unavailable to CodePeer but whose specification includes Pre/Post
+ -- conditions. The body might be unavailable for any of a number or
+ -- reasons (it is imported, the .adb file is simply missing, or the
+ -- subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
+ -- pragma). The built subprogram has the following contents:
+ -- * check preconditions
+ -- * call the subprogram
+ -- * check postconditions
+
+ function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is
+ Loc : constant Source_Ptr := Sloc (E);
+
+ function Build_Missing_Body_Decls return List_Id;
+ -- Build the declaration of the missing body subprogram and its
+ -- corresponding pragma Import.
+
+ function Build_Missing_Body_Subprogram_Call return Node_Id;
+ -- Build the call to the missing body subprogram
+
+ function Copy_Original_Specification
+ (Loc : Source_Ptr;
+ Spec : Node_Id) return Node_Id;
+ -- Build a copy of the original specification of the given subprogram
+ -- specification.
+
+ function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean;
+ -- Return True if E is a subprogram declared in a nested package that
+ -- has some formal or return type depending on a private type defined
+ -- in an enclosing package.
+
+ ------------------------------
+ -- Build_Missing_Body_Decls --
+ ------------------------------
+
+ function Build_Missing_Body_Decls return List_Id is
+ Name : constant Name_Id := Get_Contract_Only_Missing_Body_Name (E);
+ Spec : constant Node_Id := Declaration_Node (E);
+ Decl : Node_Id;
+ Prag : Node_Id;
+
+ begin
+ Decl := Make_Subprogram_Declaration (Loc,
+ Copy_Original_Specification (Loc, Spec));
+ Set_Chars (Defining_Unit_Name (Specification (Decl)), Name);
+
+ Prag :=
+ Make_Pragma (Loc,
+ Chars => Name_Import,
+ Pragma_Argument_Associations => New_List (
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Name_Ada)),
+
+ Make_Pragma_Argument_Association (Loc,
+ Expression => Make_Identifier (Loc, Name))));
+
+ return New_List (Decl, Prag);
+ end Build_Missing_Body_Decls;
+
+ ----------------------------------------
+ -- Build_Missing_Body_Subprogram_Call --
+ ----------------------------------------
+
+ function Build_Missing_Body_Subprogram_Call return Node_Id is
+ Forml : Entity_Id;
+ Parms : List_Id;
+
+ begin
+ -- Build parameter list that we need
+
+ Parms := New_List;
+ Forml := First_Formal (E);
+ while Present (Forml) loop
+ Append_To (Parms, Make_Identifier (Loc, Chars (Forml)));
+ Next_Formal (Forml);
+ end loop;
+
+ -- Build the call to the missing body subprogram
+
+ if Ekind_In (E, E_Function, E_Generic_Function) then
+ return
+ Make_Simple_Return_Statement (Loc,
+ Expression =>
+ Make_Function_Call (Loc,
+ Name => Make_Identifier (Loc,
+ Get_Contract_Only_Missing_Body_Name (E)),
+ Parameter_Associations => Parms));
+
+ else
+ return
+ Make_Procedure_Call_Statement (Loc,
+ Name => Make_Identifier (Loc,
+ Get_Contract_Only_Missing_Body_Name (E)),
+ Parameter_Associations => Parms);
+ end if;
+ end Build_Missing_Body_Subprogram_Call;
+
+ ---------------------------------
+ -- Copy_Original_Specification --
+ ---------------------------------
+
+ function Copy_Original_Specification
+ (Loc : Source_Ptr;
+ Spec : Node_Id) return Node_Id
+ is
+ function Copy_Original_Type (N : Node_Id) return Node_Id;
+ -- Duplicate the original type of a given formal or function
+ -- result type.
+
+ function Copy_Original_Type (N : Node_Id) return Node_Id is
+ begin
+ -- For expanded names located in instantiations, copy them with
+ -- semantic information (avoids visibility problems).
+
+ if In_Instance
+ and then Nkind (N) = N_Expanded_Name
+ then
+ return New_Copy_Tree (N);
+ else
+ return Copy_Separate_Tree (Original_Node (N));
+ end if;
+ end Copy_Original_Type;
+
+ -- Local variables
+
+ Current_Parameter : Node_Id;
+ Current_Identifier : Entity_Id;
+ Current_Type : Node_Id;
+ New_Identifier : Entity_Id;
+ Parameters : List_Id := No_List;
+
+ -- Start of processing for Copy_Original_Specification
+
+ begin
+ if Present (Parameter_Specifications (Spec)) then
+ Parameters := New_List;
+ Current_Parameter := First (Parameter_Specifications (Spec));
+ while Present (Current_Parameter) loop
+ Current_Identifier :=
+ Defining_Identifier (Current_Parameter);
+ Current_Type :=
+ Copy_Original_Type (Parameter_Type (Current_Parameter));
+
+ New_Identifier := Make_Defining_Identifier (Loc,
+ Chars (Current_Identifier));
+
+ Append_To (Parameters,
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier => New_Identifier,
+ Parameter_Type => Current_Type,
+ In_Present => In_Present (Current_Parameter),
+ Out_Present => Out_Present (Current_Parameter),
+ Expression =>
+ Copy_Separate_Tree (Expression (Current_Parameter))));
+
+ Next (Current_Parameter);
+ end loop;
+ end if;
+
+ case Nkind (Spec) is
+
+ when N_Function_Specification =>
+ return
+ Make_Function_Specification (Loc,
+ Defining_Unit_Name =>
+ Make_Defining_Identifier (Loc,
+ Chars => Chars (Defining_Unit_Name (Spec))),
+ Parameter_Specifications => Parameters,
+ Result_Definition =>
+ Copy_Original_Type (Result_Definition (Spec)));
+
+ when N_Procedure_Specification =>
+ return
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name =>
+ Make_Defining_Identifier (Loc,
+ Chars => Chars (Defining_Unit_Name (Spec))),
+ Parameter_Specifications => Parameters);
+
+ when others =>
+ raise Program_Error;
+ end case;
+ end Copy_Original_Specification;
+
+ -----------------------------------
+ -- Skip_Contract_Only_Subprogram --
+ -----------------------------------
+
+ function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean
+ is
+ function Depends_On_Enclosing_Private_Type return Boolean;
+ -- Return True if some formal of E (or its return type) are
+ -- private types defined in an enclosing package.
+
+ function Some_Enclosing_Package_Has_Private_Decls return Boolean;
+ -- Return True if some enclosing package of the current scope has
+ -- private declarations.
+
+ ---------------------------------------
+ -- Depends_On_Enclosing_Private_Type --
+ ---------------------------------------
+
+ function Depends_On_Enclosing_Private_Type return Boolean is
+
+ function Defined_In_Enclosing_Package
+ (Typ : Entity_Id) return Boolean;
+ -- Return True if Typ is an entity defined in an enclosing
+ -- package of the current scope.
+
+ ----------------------------------
+ -- Defined_In_Enclosing_Package --
+ ----------------------------------
+
+ function Defined_In_Enclosing_Package
+ (Typ : Entity_Id) return Boolean
+ is
+ Scop : Entity_Id := Scope (Current_Scope);
+
+ begin
+ while Scop /= Scope (Typ)
+ and then not Is_Compilation_Unit (Scop)
+ loop
+ Scop := Scope (Scop);
+ end loop;
+
+ return Scop = Scope (Typ);
+ end Defined_In_Enclosing_Package;
+
+ -- Local variables
+
+ Param_E : Entity_Id;
+ Typ : Entity_Id;
+ begin
+ Param_E := First_Entity (E);
+ while Present (Param_E) loop
+ Typ := Etype (Param_E);
+
+ if Is_Private_Type (Typ)
+ and then Defined_In_Enclosing_Package (Typ)
+ then
+ return True;
+ end if;
+
+ Next_Entity (Param_E);
+ end loop;
+
+ return Ekind (E) = E_Function
+ and then Is_Private_Type (Etype (E))
+ and then Defined_In_Enclosing_Package (Etype (E));
+ end Depends_On_Enclosing_Private_Type;
+
+ ----------------------------------------------
+ -- Some_Enclosing_Package_Has_Private_Decls --
+ ----------------------------------------------
+
+ function Some_Enclosing_Package_Has_Private_Decls return Boolean is
+ Scop : Entity_Id := Current_Scope;
+ Pkg_Spec : Node_Id := Package_Specification (Scop);
+
+ begin
+ loop
+ if Ekind (Scop) = E_Package
+ and then
+ Has_Private_Declarations (Package_Specification (Scop))
+ then
+ Pkg_Spec := Package_Specification (Scop);
+ end if;
+
+ exit when Is_Compilation_Unit (Scop);
+ Scop := Scope (Scop);
+ end loop;
+
+ return Pkg_Spec /= Package_Specification (Current_Scope);
+ end Some_Enclosing_Package_Has_Private_Decls;
+
+ -- Start of processing for Skip_Contract_Only_Subprogram
+
+ begin
+ if Ekind (Current_Scope) = E_Package
+ and then Some_Enclosing_Package_Has_Private_Decls
+ and then Depends_On_Enclosing_Private_Type
+ then
+ if Debug_Flag_Dot_KK then
+ declare
+ Saved_Mode : constant Warning_Mode_Type := Warning_Mode;
+
+ begin
+ -- Warnings are disabled by default under CodePeer_Mode
+ -- (see switch-c). Enable them temporarily.
+
+ Warning_Mode := Normal;
+ Error_Msg_N
+ ("cannot generate contract-only subprogram?", E);
+ Warning_Mode := Saved_Mode;
+ end;
+ end if;
+
+ return True;
+ end if;
+
+ return False;
+ end Skip_Contract_Only_Subprogram;
+
+ -- Start of processing for Build_Contract_Only_Subprogram
+
+ begin
+ -- Test cases where the wrapper is not needed and cases where we
+ -- cannot build the wrapper.
+
+ if not CodePeer_Mode
+ or else Inside_A_Generic
+ or else not Is_Subprogram (E)
+ or else Is_Abstract_Subprogram (E)
+ or else Is_Imported (E)
+ or else No (Contract (E))
+ or else No (Pre_Post_Conditions (Contract (E)))
+ or else Is_Contract_Only_Body (E)
+ or else Skip_Contract_Only_Subprogram (E)
+ or else Convention (E) = Convention_Protected
+ then
+ return Empty;
+ end if;
+
+ -- Note on calls to Copy_Separate_Tree. The trees we are copying
+ -- here are fully analyzed, but we definitely want fully syntactic
+ -- unanalyzed trees in the body we construct, so that the analysis
+ -- generates the right visibility, and that is exactly what the
+ -- calls to Copy_Separate_Tree give us.
+
+ declare
+ Name : constant Name_Id := Get_Contract_Only_Body_Name (E);
+ Id : Entity_Id;
+ Bod : Node_Id;
+
+ begin
+ Bod :=
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Copy_Original_Specification (Loc, Declaration_Node (E)),
+ Declarations =>
+ Build_Missing_Body_Decls,
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => New_List (
+ Build_Missing_Body_Subprogram_Call),
+ End_Label => Make_Identifier (Loc, Name)));
+
+ Id := Defining_Unit_Name (Specification (Bod));
+
+ -- Copy only the pre/postconditions of the original contract
+ -- since it is what we need, but also because pragmas stored in
+ -- the other fields have N_Pragmas with N_Aspect_Specifications
+ -- that reference their associated pragma (thus causing an endless
+ -- loop when trying to copy the subtree).
+
+ declare
+ New_Contract : constant Node_Id := Make_Contract (Sloc (E));
+
+ begin
+ Set_Pre_Post_Conditions (New_Contract,
+ Copy_Separate_Tree (Pre_Post_Conditions (Contract (E))));
+ Set_Contract (Id, New_Contract);
+ end;
+
+ -- Fix the name of this new subprogram and link the original
+ -- subprogram with its Contract_Only_Body subprogram.
+
+ Set_Chars (Id, Name);
+ Set_Is_Contract_Only_Body (Id);
+ Set_Contract_Only_Body (E, Id);
+
+ return Bod;
+ end;
+ end Build_Contract_Only_Subprogram;
+
+ -------------------------------------
+ -- Build_Contract_Only_Subprograms --
+ -------------------------------------
+
+ function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is
+ Decl : Node_Id;
+ Subp_Id : Entity_Id;
+ New_Subp : Node_Id;
+ Result : List_Id := No_List;
+
+ begin
+ Decl := First (L);
+ while Present (Decl) loop
+ if Nkind (Decl) = N_Subprogram_Declaration then
+ Subp_Id := Defining_Unit_Name (Specification (Decl));
+ New_Subp := Build_Contract_Only_Subprogram (Subp_Id);
+
+ if Present (New_Subp) then
+ if No (Result) then
+ Result := New_List;
+ end if;
+
+ Append_To (Result, New_Subp);
+ end if;
+ end if;
+
+ Next (Decl);
+ end loop;
+
+ return Result;
+ end Build_Contract_Only_Subprograms;
+
+ ------------------------------
+ -- Has_Private_Declarations --
+ ------------------------------
+
+ function Has_Private_Declarations (N : Node_Id) return Boolean is
+ begin
+ if not Nkind_In (N, N_Package_Specification,
+ N_Task_Definition,
+ N_Protected_Definition)
+ then
+ return False;
+ else
+ return Present (Private_Declarations (N))
+ and then Is_Non_Empty_List (Private_Declarations (N));
+ end if;
+ end Has_Private_Declarations;
+
+ -- Local variables
+
+ Subp_List : List_Id;
+
+ -- Start of processing for Build_And_Analyze_Contract_Only_Subprograms
+
+ begin
+ Subp_List := Build_Contract_Only_Subprograms (L);
+ Append_Contract_Only_Subprograms (Subp_List);
+ Analyze_Contract_Only_Subprograms (L);
+ end Build_And_Analyze_Contract_Only_Subprograms;
+
end Contracts;
-- d.H GNSA mode for ASIS
-- d.I Do not ignore enum representation clauses in CodePeer mode
-- d.J Disable parallel SCIL generation mode
- -- d.K
+ -- d.K Enable generation of contract-only procedures in CodePeer mode
-- d.L Depend on back end for limited types in if and case expressions
-- d.M Relaxed RM semantics
-- d.N Add node to all entities
-- done in parallel to speed processing. This switch disables this
-- behavior.
+ -- d.K Enable generation of contract-only procedures in CodePeer mode and
+ -- report a warning on subprograms for which the contract-only body
+ -- cannot be built. Currently reported on subprograms defined in
+ -- nested package specs that have some formal (or return type) whose
+ -- type is a private type defined in some enclosing package and that
+ -- have pre/postconditions.
+
-- d.L Normally the front end generates special expansion for conditional
-- expressions of a limited type. This debug flag removes this special
-- case expansion, leaving it up to the back end to handle conditional
Rewrite (N, Make_Integer_Literal (Loc, 0));
end if;
- Analyze (N);
+ -- Due to cases where the entity type of the attribute is already
+ -- resolved the rewritten N must get re-resolved to its appropriate
+ -- type.
+
+ Analyze_And_Resolve (N, Typ);
end Finalization_Size;
-----------
-- For an element iterator, the Element aspect must be present,
-- (this is checked during analysis) and the expansion takes the form:
- -- Cursor : Cursor_type := First (Container);
+ -- Cursor : Cursor_Type := First (Container);
-- Elmt : Element_Type;
-- while Has_Element (Cursor, Container) loop
-- Elmt := Element (Container, Cursor);
-- In that case we create a block to hold a variable declaration
-- initialized with a call to Element, and generate:
- -- Cursor : Cursor_type := First (Container);
+ -- Cursor : Cursor_Type := First (Container);
-- while Has_Element (Cursor, Container) loop
-- declare
- -- Elmt : Element-Type := Element (Container, Cursor);
+ -- Elmt : Element_Type := Element (Container, Cursor);
-- begin
-- <original loop statements>
-- Cursor := Next (Container, Cursor);
Set_Ekind (Cursor, E_Variable);
Insert_Action (N, Init);
- -- Declaration for Element.
+ -- Declaration for Element
Elmt_Decl :=
Make_Object_Declaration (Loc,
-- expression for the value of the actual, EF is the entity for the
-- extra formal.
- procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id);
+ procedure Add_View_Conversion_Invariants
+ (Formal : Entity_Id;
+ Actual : Node_Id);
-- Adds invariant checks for every intermediate type between the range
-- of a view converted argument to its ancestor (from parent to child).
end if;
end Add_Extra_Actual;
- ---------------------------
- -- Check_View_Conversion --
- ---------------------------
+ ------------------------------------
+ -- Add_View_Conversion_Invariants --
+ ------------------------------------
- procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id) is
+ procedure Add_View_Conversion_Invariants
+ (Formal : Entity_Id;
+ Actual : Node_Id)
+ is
Arg : Entity_Id;
Curr_Typ : Entity_Id;
Inv_Checks : List_Id;
if not Is_Empty_List (Inv_Checks) then
Insert_Actions_After (N, Inv_Checks);
end if;
- end Check_View_Conversion;
+ end Add_View_Conversion_Invariants;
---------------------------
-- Inherited_From_Formal --
Duplicate_Subexpr_Move_Checks (Actual)));
end if;
- -- Invariant checks are performed for every intermediate type between
- -- the range of a view converted argument to its ancestor (from
- -- parent to child) if it is passed as an "out" or "in out" parameter
- -- after executing the call (RM 7.3.2 (12/3, 13/3, 14/3)).
+ -- Perform invariant checks for all intermediate types in a view
+ -- conversion after successful return from a call that passes the
+ -- view conversion as an IN OUT or OUT parameter (RM 7.3.2 (12/3,
+ -- 13/3, 14/3)). Consider only source conversion in order to avoid
+ -- generating spurious checks on complex expansion such as object
+ -- initialization through an extension aggregate.
- if Ekind (Formal) /= E_In_Parameter
+ if Comes_From_Source (N)
+ and then Ekind (Formal) /= E_In_Parameter
and then Nkind (Actual) = N_Type_Conversion
then
- Check_View_Conversion (Formal, Actual);
+ Add_View_Conversion_Invariants (Formal, Actual);
end if;
-- This label is required when skipping extra actual generation for
-- --
-- S p e c --
-- --
--- Copyright (C) 1992-2011, Free Software Foundation, Inc. --
+-- Copyright (C) 1992-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
function Build_Abort_Block_Handler (Loc : Source_Ptr) return Node_Id;
-- Generate if front-end exception:
-- when others =>
- -- Abort_Under;
+ -- Abort_Undefer;
-- or if back-end exception:
-- when others =>
-- null;
-- Otherwise the renamed object denotes a name
else
- Rewrite (N, New_Copy_Tree (Obj_Id));
+ Rewrite (N, New_Copy_Tree (Obj_Id, New_Sloc => Loc));
Reset_Analyzed_Flags (N);
end if;
Set_Corresponding_Spec (Proc_Body, Proc_Id);
-- The body should not be inserted into the tree when the context is
- -- ASIS, GNATprove or a generic unit because it is not part of the
- -- template. Note that the body must still be generated in order to
- -- resolve the DIC assertion expression.
+ -- ASIS or a generic unit because it is not part of the template. Note
+ -- that the body must still be generated in order to resolve the DIC
+ -- assertion expression.
- if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
+ if ASIS_Mode or Inside_A_Generic then
null;
+ -- Semi-insert the body into the tree for GNATprove by setting its
+ -- Parent field. This allows for proper upstream tree traversals.
+
+ elsif GNATprove_Mode then
+ Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+
-- Otherwise the body is part of the freezing actions of the working
-- type.
New_Occurrence_Of (Work_Typ, Loc)))));
-- The declaration should not be inserted into the tree when the context
- -- is ASIS, GNATprove, or a generic unit because it is not part of the
- -- template.
+ -- is ASIS or a generic unit because it is not part of the template.
- if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
+ if ASIS_Mode or Inside_A_Generic then
null;
+ -- Semi-insert the declaration into the tree for GNATprove by setting
+ -- its Parent field. This allows for proper upstream tree traversals.
+
+ elsif GNATprove_Mode then
+ Set_Parent (Proc_Decl, Parent (Typ_Decl));
+
-- Otherwise insert the declaration
else
- pragma Assert (Present (Typ_Decl));
Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
end if;
-- AD Elaborate_All_Desirable set for this unit, which means that
-- there is no Elaborate_All, but the analysis suggests that
-- Program_Error may be raised if the Elaborate_All conditions
- -- cannot be satisfied. In dynamic elaboration mode, the binder
- -- will attempt to treat AD as EA if it can. In static
- -- elaboration mode, the binder will treat AD as EA, even if it
- -- introduces cycles.
+ -- cannot be satisfied. The binder will attempt to treat AD as
+ -- EA if it can.
-- The parameter source-name and lib-name are omitted for the case of a
-- generic unit compiled with earlier versions of GNAT which did not
-- --
-- B o d y --
-- --
--- Copyright (C) 2010-2012, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- --
------------------------------------------------------------------------------
-with Alloc; use Alloc;
-with Atree; use Atree;
-with Opt; use Opt;
-with Sinfo; use Sinfo;
-with Table;
+with Atree; use Atree;
+with Opt; use Opt;
+with Sinfo; use Sinfo;
+with System.HTable; use System.HTable;
package body SCIL_LL is
+ Contract_Only_Body_Suffix : constant String := "__contract_only";
+ -- Suffix of Contract_Only_Body subprograms internally built only under
+ -- CodePeer mode
+
+ Contract_Only_Missing_Body_Suffix : constant String := "__missing_body";
+ -- Suffix of Contract_Only_Missing_Body subprograms internally built only
+ -- under CodePeer mode
procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id);
-- Copy the SCIL field from Source to Target (it is used as the argument
-- for a call to Set_Reporting_Proc in package atree).
- function SCIL_Nodes_Table_Size return Pos;
- -- Used to initialize the table of SCIL nodes because we do not want
- -- to consume memory for this table if it is not required.
+ type Header_Num is range 1 .. 4096;
+
+ function Hash (N : Node_Id) return Header_Num;
+ -- Hash function for Node_Ids
+
+ --------------------------
+ -- Internal Hash Tables --
+ --------------------------
+
+ package Contract_Only_Body_Flag is new Simple_HTable
+ (Header_Num => Header_Num,
+ Element => Boolean,
+ No_Element => False,
+ Key => Node_Id,
+ Hash => Hash,
+ Equal => "=");
+ -- This table records the value of flag Is_Contract_Only_Flag of tree nodes
+
+ package Contract_Only_Body_Nodes is new Simple_HTable
+ (Header_Num => Header_Num,
+ Element => Node_Id,
+ No_Element => Empty,
+ Key => Node_Id,
+ Hash => Hash,
+ Equal => "=");
+ -- This table records the value of attribute Contract_Only_Body of tree
+ -- nodes.
+
+ package SCIL_Nodes is new Simple_HTable
+ (Header_Num => Header_Num,
+ Element => Node_Id,
+ No_Element => Empty,
+ Key => Node_Id,
+ Hash => Hash,
+ Equal => "=");
+ -- This table records the value of attribute SCIL_Node of tree nodes.
+
+ --------------------
+ -- Copy_SCIL_Node --
+ --------------------
+
+ procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id) is
+ begin
+ Set_SCIL_Node (Target, Get_SCIL_Node (Source));
+ end Copy_SCIL_Node;
----------------------------
- -- SCIL_Nodes_Table_Size --
+ -- Get_Contract_Only_Body --
----------------------------
- function SCIL_Nodes_Table_Size return Pos is
+ function Get_Contract_Only_Body (N : Node_Id) return Node_Id is
begin
- if Generate_SCIL then
- return Alloc.Orig_Nodes_Initial;
+ if CodePeer_Mode
+ and then Present (N)
+ then
+ return Contract_Only_Body_Nodes.Get (N);
else
- return 1;
+ return Empty;
end if;
- end SCIL_Nodes_Table_Size;
-
- package SCIL_Nodes is new Table.Table (
- Table_Component_Type => Node_Id,
- Table_Index_Type => Node_Id'Base,
- Table_Low_Bound => First_Node_Id,
- Table_Initial => SCIL_Nodes_Table_Size,
- Table_Increment => Alloc.Orig_Nodes_Increment,
- Table_Name => "SCIL_Nodes");
- -- This table records the value of attribute SCIL_Node of all the
- -- tree nodes.
+ end Get_Contract_Only_Body;
- --------------------
- -- Copy_SCIL_Node --
- --------------------
+ ---------------------------------
+ -- Get_Contract_Only_Body_Name --
+ ---------------------------------
- procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id) is
+ function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id is
begin
- Set_SCIL_Node (Target, Get_SCIL_Node (Source));
- end Copy_SCIL_Node;
+ return Name_Find (Get_Name_String (Chars (E)) &
+ Contract_Only_Body_Suffix);
+ end Get_Contract_Only_Body_Name;
- ----------------
- -- Initialize --
- ----------------
+ -----------------------------------------
+ -- Get_Contract_Only_Missing_Body_Name --
+ -----------------------------------------
- procedure Initialize is
+ function Get_Contract_Only_Missing_Body_Name (E : Entity_Id)
+ return Name_Id is
begin
- SCIL_Nodes.Init;
- Set_Reporting_Proc (Copy_SCIL_Node'Access);
- end Initialize;
+ return Name_Find (Get_Name_String (Chars (E)) &
+ Contract_Only_Missing_Body_Suffix);
+ end Get_Contract_Only_Missing_Body_Name;
-------------------
-- Get_SCIL_Node --
if Generate_SCIL
and then Present (N)
then
- return SCIL_Nodes.Table (N);
+ return SCIL_Nodes.Get (N);
else
return Empty;
end if;
end Get_SCIL_Node;
+ ----------
+ -- Hash --
+ ----------
+
+ function Hash (N : Node_Id) return Header_Num is
+ begin
+ return Header_Num (1 + N mod Node_Id (Header_Num'Last));
+ end Hash;
+
+ ----------------
+ -- Initialize --
+ ----------------
+
+ procedure Initialize is
+ begin
+ SCIL_Nodes.Reset;
+ Contract_Only_Body_Nodes.Reset;
+ Contract_Only_Body_Flag.Reset;
+ Set_Reporting_Proc (Copy_SCIL_Node'Access);
+ end Initialize;
+
+ ---------------------------
+ -- Is_Contract_Only_Body --
+ ---------------------------
+
+ function Is_Contract_Only_Body (E : Entity_Id) return Boolean is
+ begin
+ return Contract_Only_Body_Flag.Get (E);
+ end Is_Contract_Only_Body;
+
+ ----------------------------
+ -- Set_Contract_Only_Body --
+ ----------------------------
+
+ procedure Set_Contract_Only_Body (N : Node_Id; Value : Node_Id) is
+ begin
+ pragma Assert (CodePeer_Mode
+ and then Present (N)
+ and then Is_Contract_Only_Body (Value));
+
+ Contract_Only_Body_Nodes.Set (N, Value);
+ end Set_Contract_Only_Body;
+
+ -------------------------------
+ -- Set_Is_Contract_Only_Body --
+ -------------------------------
+
+ procedure Set_Is_Contract_Only_Body (E : Entity_Id) is
+ begin
+ Contract_Only_Body_Flag.Set (E, True);
+ end Set_Is_Contract_Only_Body;
+
-------------------
-- Set_SCIL_Node --
-------------------
end case;
end if;
- if Atree.Last_Node_Id > SCIL_Nodes.Last then
- SCIL_Nodes.Set_Last (Atree.Last_Node_Id);
- end if;
-
- SCIL_Nodes.Set_Item (N, Value);
+ SCIL_Nodes.Set (N, Value);
end Set_SCIL_Node;
end SCIL_LL;
-- --
-- S p e c --
-- --
--- Copyright (C) 2010, Free Software Foundation, Inc. --
+-- Copyright (C) 2010-2016, Free Software Foundation, Inc. --
-- --
-- GNAT is free software; you can redistribute it and/or modify it under --
-- terms of the GNU General Public License as published by the Free Soft- --
-- --
------------------------------------------------------------------------------
--- This package extends the tree nodes with a field that is used to reference
--- the SCIL node.
+-- This package extends the tree nodes with fields that are used to reference
+-- the SCIL node and the Contract_Only_Body of a subprogram with aspects.
+with Namet; use Namet;
with Types; use Types;
package SCIL_LL is
+ function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id;
+ -- Return the name of the Contract_Only_Body subprogram of E
+
+ function Get_Contract_Only_Missing_Body_Name (E : Entity_Id) return Name_Id;
+ -- Return the name of the Contract_Only_Missing_Body subprogram of E
+
+ function Get_Contract_Only_Body (N : Node_Id) return Node_Id;
+ -- Read the value of attribute Contract_Only_Body
+
function Get_SCIL_Node (N : Node_Id) return Node_Id;
-- Read the value of attribute SCIL node
+ procedure Set_Contract_Only_Body (N : Node_Id; Value : Node_Id);
+ -- Set the value of attribute Contract_Only_Body
+
procedure Set_SCIL_Node (N : Node_Id; Value : Node_Id);
-- Set the value of attribute SCIL node
procedure Initialize;
-- Initialize the table of SCIL nodes
+ function Is_Contract_Only_Body (E : Entity_Id) return Boolean;
+ -- Return True if E is a Contract_Only_Body subprogram
+
+ procedure Set_Is_Contract_Only_Body (E : Entity_Id);
+ -- Set E as Contract_Only_Body subprogram
+
end SCIL_LL;
-- See Sem_Ch10 (Install_Parents, Remove_Parents).
Node_To_Be_Wrapped : Node_Id;
- -- Only used in transient scopes. Records the node which will
- -- be wrapped by the transient block.
+ -- Only used in transient scopes. Records the node which will be wrapped
+ -- by the transient block.
Actions_To_Be_Wrapped : Scope_Actions;
-- Actions that have to be inserted at the start, at the end, or as
-- Valid_Array_Conversion --
----------------------------
- function Valid_Array_Conversion return Boolean
- is
+ function Valid_Array_Conversion return Boolean is
Opnd_Comp_Type : constant Entity_Id := Component_Type (Opnd_Type);
Opnd_Comp_Base : constant Entity_Id := Base_Type (Opnd_Comp_Type);
else
Get_Next_Interp (I, It);
end if;
-
end loop;
All_Interp.Table (All_Interp.Last) := (Name, Typ, Abstr_Op);
projects / gcc.git / commitdiff