+ ------------------
+ -- Process_PPCs --
+ ------------------
+
+ procedure Process_PPCs
+ (N : Node_Id;
+ Spec_Id : Entity_Id;
+ Body_Id : Entity_Id)
+ is
+ Loc : constant Source_Ptr := Sloc (N);
+ Prag : Node_Id;
+ Plist : List_Id := No_List;
+ Subp : Entity_Id;
+ Parms : List_Id;
+
+ function Grab_PPC (Nam : Name_Id) return Node_Id;
+ -- Prag contains an analyzed precondition or postcondition pragma.
+ -- This function copies the pragma, changes it to the corresponding
+ -- Check pragma and returns the Check pragma as the result. The
+ -- argument Nam is either Name_Precondition or Name_Postcondition.
+
+ --------------
+ -- Grab_PPC --
+ --------------
+
+ function Grab_PPC (Nam : Name_Id) return Node_Id is
+ CP : constant Node_Id := New_Copy_Tree (Prag);
+
+ begin
+ -- Set Analyzed to false, since we want to reanalyze the check
+ -- procedure. Note that it is only at the outer level that we
+ -- do this fiddling, for the spec cases, the already preanalyzed
+ -- parameters are not affected.
+
+ Set_Analyzed (CP, False);
+
+ -- Change pragma into corresponding pragma Check
+
+ Prepend_To (Pragma_Argument_Associations (CP),
+ Make_Pragma_Argument_Association (Sloc (Prag),
+ Expression =>
+ Make_Identifier (Loc,
+ Chars => Nam)));
+ Set_Pragma_Identifier (CP,
+ Make_Identifier (Sloc (Prag),
+ Chars => Name_Check));
+
+ return CP;
+ end Grab_PPC;
+
+ -- Start of processing for Process_PPCs
+
+ begin
+ -- Grab preconditions from spec
+
+ if Present (Spec_Id) then
+
+ -- Loop through PPC pragmas from spec. Note that preconditions from
+ -- the body will be analyzed and converted when we scan the body
+ -- declarations below.
+
+ Prag := Spec_PPC_List (Spec_Id);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Precondition
+ and then PPC_Enabled (Prag)
+ then
+ -- Add pragma Check at the start of the declarations of N.
+ -- Note that this processing reverses the order of the list,
+ -- which is what we want since new entries were chained to
+ -- the head of the list.
+
+ Prepend (Grab_PPC (Name_Precondition), Declarations (N));
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- Build postconditions procedure if needed and prepend the following
+ -- declaration to the start of the declarations for the subprogram.
+
+ -- procedure _postconditions [(_Result : resulttype)] is
+ -- begin
+ -- pragma Check (Postcondition, condition [,message]);
+ -- pragma Check (Postcondition, condition [,message]);
+ -- ...
+ -- end;
+
+ -- First we deal with the postconditions in the body
+
+ if Is_Non_Empty_List (Declarations (N)) then
+
+ -- Loop through declarations
+
+ Prag := First (Declarations (N));
+ while Present (Prag) loop
+ if Nkind (Prag) = N_Pragma then
+
+ -- If pragma, capture if enabled postcondition, else ignore
+
+ if Pragma_Name (Prag) = Name_Postcondition
+ and then Check_Enabled (Name_Postcondition)
+ then
+ if Plist = No_List then
+ Plist := Empty_List;
+ end if;
+
+ Analyze (Prag);
+ Append (Grab_PPC (Name_Postcondition), Plist);
+ end if;
+
+ Next (Prag);
+
+ -- Not a pragma, if comes from source, then end scan
+
+ elsif Comes_From_Source (Prag) then
+ exit;
+
+ -- Skip stuff not coming from source
+
+ else
+ Next (Prag);
+ end if;
+ end loop;
+ end if;
+
+ -- Now deal with any postconditions from the spec
+
+ if Present (Spec_Id) then
+
+ -- Loop through PPC pragmas from spec
+
+ Prag := Spec_PPC_List (Spec_Id);
+ while Present (Prag) loop
+ if Pragma_Name (Prag) = Name_Postcondition
+ and then PPC_Enabled (Prag)
+ then
+ if Plist = No_List then
+ Plist := Empty_List;
+ end if;
+
+ Append (Grab_PPC (Name_Postcondition), Plist);
+ end if;
+
+ Prag := Next_Pragma (Prag);
+ end loop;
+ end if;
+
+ -- If we had any postconditions, build the procedure
+
+ if Present (Plist) then
+ Subp := Defining_Entity (N);
+
+ if Etype (Subp) /= Standard_Void_Type then
+ Parms := New_List (
+ Make_Parameter_Specification (Loc,
+ Defining_Identifier =>
+ Make_Defining_Identifier (Loc,
+ Chars => Name_uResult),
+ Parameter_Type => New_Occurrence_Of (Etype (Subp), Loc)));
+ else
+ Parms := No_List;
+ end if;
+
+ Prepend_To (Declarations (N),
+ Make_Subprogram_Body (Loc,
+ Specification =>
+ Make_Procedure_Specification (Loc,
+ Defining_Unit_Name =>
+ Make_Defining_Identifier (Loc,
+ Chars => Name_uPostconditions),
+ Parameter_Specifications => Parms),
+
+ Declarations => Empty_List,
+
+ Handled_Statement_Sequence =>
+ Make_Handled_Sequence_Of_Statements (Loc,
+ Statements => Plist)));
+
+ if Present (Spec_Id) then
+ Set_Has_Postconditions (Spec_Id);
+ else
+ Set_Has_Postconditions (Body_Id);
+ end if;
+ end if;
+ end Process_PPCs;
+