Commit 63d92af8 authored by jjhugues's avatar jjhugues
Browse files

* Correct generation of Ada2012/SPARK2014 aspects

	For openaadl/ocarina#131
parent 737bae87
......@@ -221,7 +221,18 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
Make_Defining_Identifier (Map_Port_Interface_Name (E)),
Parameter_Mode => Mode_Inout)
),
Aspect_Specification => Runtime_Spec_Aspect_Definition);
Aspect_Specification =>
Make_Aspect_Specification
(Make_List_Id
(Make_Aspect
(ASN (A_Global),
Make_Global_Specification
(Make_List_Id
(Make_Moded_Global_List
(Mode_In,
Make_Defining_Identifier
(PN (P_Elaborated_Variables)))))))));
return N;
end Get_Value_Spec;
......@@ -1908,12 +1919,12 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
-- Build a string literal for the pragma Warnings On|Off:
--
-- if there is no error management, and the
-- If there is no error recovery function, and the
-- current subprogram is a function, we need to shut
-- down the warning on missing return: by construction
-- of the source code, there cannot be situation in
-- which we exit without entering one of the if
-- statemetns.
-- statements.
Set_Str_To_Name_Buffer ("*return*");
Pragma_Warnings_Off_Value := New_String_Value (Name_Find);
......
......@@ -707,30 +707,6 @@ package body Ocarina.Backends.PO_HI_Ada.Job is
The_System : constant Node_Id :=
Parent_Component (Parent_Subcomponent (E));
function Package_Spec_Aspect_Definition return Node_Id is
begin
if Add_SPARK2014_Annotations then
return Make_Aspect_Specification
(Make_List_Id
(Make_Aspect (ASN (A_Initializes),
Make_Initialization_Spec
(Make_List_Id
(Make_Defining_Identifier
(PN (P_Elaborated_Variables))))),
Make_Aspect
(ASN (A_Abstract_State),
Make_Abstract_State_List
(Make_List_Id
(Make_State_Name_With_Option
(Make_Defining_Identifier
(PN (P_Elaborated_Variables)),
Synchronous => True,
External => True))))));
else
return No_Node;
end if;
end Package_Spec_Aspect_Definition;
begin
Push_Entity (P);
Push_Entity (U);
......@@ -766,9 +742,6 @@ package body Ocarina.Backends.PO_HI_Ada.Job is
-- the scheduler is set to non-preemptive mode.
end if;
ADN.Set_Aspect_Specification (Current_Package,
Package_Spec_Aspect_Definition);
-- Visit all the subcomponents of the process
if not AINU.Is_Empty (Subcomponents (E)) then
......@@ -1112,8 +1085,6 @@ package body Ocarina.Backends.PO_HI_Ada.Job is
-- are appended after all entities generated for threads since
-- they need visibility on these entities.
Package_Body_Refined_States : List_Id := No_List;
-------------------
-- Task_Job_Body --
-------------------
......@@ -2801,24 +2772,6 @@ package body Ocarina.Backends.PO_HI_Ada.Job is
The_System : constant Node_Id :=
Parent_Component (Parent_Subcomponent (E));
function Package_Body_Aspect_Definition return Node_Id is
begin
if Add_SPARK2014_Annotations then
return Make_Aspect_Specification
(Make_List_Id
(Make_Aspect
(ASN (A_Refined_State),
Make_Refinement_List
(Make_List_Id
(Make_Refinement_Clause
(Make_Defining_Identifier
(PN (P_Elaborated_Variables)),
Package_Body_Refined_States))))));
else
return No_Node;
end if;
end Package_Body_Aspect_Definition;
begin
Push_Entity (P);
Push_Entity (U);
......@@ -2838,7 +2791,6 @@ package body Ocarina.Backends.PO_HI_Ada.Job is
-- Initialize the runtime routine list
Interrogation_Routine_List := New_List (ADN.K_Statement_List);
Package_Body_Refined_States := New_List (ADN.K_List_Id);
-- Visit all the subcomponents of the process
......@@ -2931,10 +2883,6 @@ package body Ocarina.Backends.PO_HI_Ada.Job is
end loop;
end if;
ADN.Set_Aspect_Specification
(Current_Package,
Package_Body_Aspect_Definition);
-- Unmark all the marked types
Reset_Handlings;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment