Skip to content
GitLab
Commit 92057e35 authored by yoogx's avatar yoogx
Browse files

* Add support for Ada2012 aspects, implement generation of 

          selected Ada2012 and SPARK2014 aspects

          For openaadl/ocarina#131
parent c134071c
Hide whitespace changes
Inline Side-by-side
src/backends/ast_ada/ocarina-backends-ada_tree-generator.adb
View file @ 92057e35
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2015 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2018 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -50,6 +50,7 @@ package body Ocarina.Backends.Ada_Tree.Generator is
procedure Generate_Access_Type_Definition (N : Node_Id);
procedure Generate_Ada_Comment (N : Node_Id);
procedure Generate_Aspect (N : Node_Id);
procedure Generate_HI_Distributed_Application (N : Node_Id);
procedure Generate_HI_Node (N : Node_Id);
procedure Generate_Unit_Packages (N : Node_Id);
......@@ -1603,6 +1604,9 @@ package body Ocarina.Backends.Ada_Tree.Generator is
Write_Space;
Generate (Defining_Identifier (Package_Declaration (N)));
Write_Space;
Generate_Aspect (Aspect_Specification (N));
Write (Tok_Is);
Write_Eol (2);
......@@ -1733,6 +1737,8 @@ package body Ocarina.Backends.Ada_Tree.Generator is
Write (Tok_Package);
Write_Space;
Generate (Defining_Identifier (Package_Declaration (N)));
Generate_Aspect (Aspect_Specification (N));
Write_Space;
Write (Tok_Is);
Write_Eol (2);
......@@ -2392,8 +2398,171 @@ package body Ocarina.Backends.Ada_Tree.Generator is
Generate (G);
Decrement_Indentation;
end if;
Generate_Aspect (Aspect_Specification (N));
end Generate_Subprogram_Specification;
---------------------
-- Generate_Aspect --
---------------------
procedure Generate_Aspect (N : Node_Id) is
W : Node_Id;
begin
if Present (N) and then
not Is_Empty (Aspect (N))
then
Write_Eol;
Increment_Indentation;
Write_Indentation;
Write (Tok_With);
Write_Space;
W := First_Node (Aspect (N));
while Present (W) loop
Write_Name (Aspect_Mark (W));
if Present (Aspect_Definition (W)) then
if Kind (Aspect_Definition (W)) = K_Pre_Definition then
Write_Space;
Write (Tok_Arrow);
Write_Space;
Write (Tok_Left_Paren);
Generate (Subprogram_Call (Aspect_Definition (W)));
Write (Tok_Right_Paren);
elsif Kind (Aspect_Definition (W)) = K_Global_Specification then
declare
X : Node_Id;
begin
X := First_Node (Moded_Global_List
(Aspect_Definition (W)));
while (Present (X)) loop
Write_Space;
Write (Tok_Arrow);
Write_Space;
Write (Tok_Left_Paren);
if Mode_Selector (X) = Mode_In then
Write_Str ("Input => ");
else
raise Program_Error;
end if;
Write (Tok_Left_Paren);
Generate (Defining_Identifier (X));
Write (Tok_Right_Paren);
Write (Tok_Right_Paren);
X := Next_Node (X);
end loop;
end;
elsif Kind (Aspect_Definition (W)) = K_Initialization_Spec then
declare
X : Node_Id;
begin
X := First_Node (Initialization_List
(Aspect_Definition (W)));
while (Present (X)) loop
Write_Space;
Write (Tok_Arrow);
Write_Space;
Write (Tok_Left_Paren);
Generate (X);
Write (Tok_Right_Paren);
X := Next_Node (X);
exit when No (W);
end loop;
end;
elsif Kind (Aspect_Definition (W)) = K_Abstract_State_List then
declare
X : Node_Id;
begin
X := First_Node (State_Name_With_Option
(Aspect_Definition (W)));
while (Present (X)) loop
Write_Space;
Write (Tok_Arrow);
Write_Space;
Write (Tok_Left_Paren);
Generate (Defining_Identifier (X));
if Synchronous (X) or else External (X) then
Write_Space;
Write (Tok_With);
Write_Space;
if Synchronous (X) then
Write_Str ("Synchronous");
end if;
if Synchronous (X) and then External (X) then
Write_Str (", ");
end if;
if External (X) then
Write_Str ("External");
end if;
end if;
Write (Tok_Right_Paren);
X := Next_Node (X);
exit when No (W);
end loop;
end;
elsif Kind (Aspect_Definition (W)) = K_Refinement_List then
declare
X : Node_Id;
begin
X := First_Node (Refinement_Clause
(Aspect_Definition (W)));
while (Present (X)) loop
Write_Space;
Write (Tok_Arrow);
Write_Space;
Write (Tok_Left_Paren);
Generate (State_Name (X));
declare
Y : Node_Id;
begin
Y := First_Node (Constituent (X));
if Present (Y) then
Write_Space;
Write (Tok_Arrow);
Write_Eol;
Write_Indentation (9);
Write (Tok_Left_Paren);
end if;
while (Present (Y)) loop
Generate (Y);
Y := Next_Node (Y);
exit when No (Y);
Write (Tok_Comma);
Write_Eol;
Write_Indentation (10);
end loop;
end;
Write (Tok_Right_Paren);
X := Next_Node (X);
exit when No (W);
end loop;
Write (Tok_Right_Paren);
end;
end if;
end if;
W := Next_Node (W);
exit when No (W);
Write (Tok_Comma);
Write_Eol;
Write_Indentation (5);
end loop;
Decrement_Indentation;
Write_Space;
end if;
end Generate_Aspect;
------------------------------
-- Generate_Type_Conversion --
------------------------------
......
src/backends/ast_ada/ocarina-backends-ada_tree-nutils.adb
View file @ 92057e35
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2016 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2018 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -923,6 +923,13 @@ package body Ocarina.Backends.Ada_Tree.Nutils is
GNAT.Case_Util.To_Mixed (Name_Buffer (1 .. Name_Len));
EN (E) := Name_Find;
end loop;
for A in Aspect_Id loop
Set_Str_To_Name_Buffer (Aspect_Id'Image (A));
Set_Str_To_Name_Buffer (Name_Buffer (3 .. Name_Len));
GNAT.Case_Util.To_Mixed (Name_Buffer (1 .. Name_Len));
ASN (A) := Name_Find;
end loop;
end Initialize;
-----------
......@@ -1071,6 +1078,148 @@ package body Ocarina.Backends.Ada_Tree.Nutils is
return N;
end Make_Array_Type_Definition;
-------------------------------
-- Make_Aspect_Specification --
-------------------------------
function Make_Aspect_Specification (Aspects : List_Id) return Node_Id is
N : Node_Id;
begin
N := New_Node (ADN.K_Aspect_Specification);
Set_Aspect (N, Aspects);
return N;
end Make_Aspect_Specification;
--------------
-- Make_Pre --
--------------
function Make_Pre (Subprogram_Call : Node_Id) return Node_Id is
N : Node_Id;
begin
N := New_Node (ADN.K_Pre_Definition);
Set_Subprogram_Call (N, Subprogram_Call);
return N;
end Make_Pre;
-------------------------------
-- Make_Global_Specification --
-------------------------------
function Make_Global_Specification
(Moded_Global_List : List_Id)
return Node_Id
is
N : Node_Id;
begin
N := New_Node (ADN.K_Global_Specification);
Set_Moded_Global_List (N, Moded_Global_List);
return N;
end Make_Global_Specification;
function Make_Moded_Global_List
(Mode : Mode_Id; Identifier : Node_Id) return Node_Id
is
N : Node_Id;
begin
N := New_Node (ADN.K_Moded_Global_List);
Set_Mode_Selector (N, Mode);
Set_Defining_Identifier (N, Identifier);
return N;
end Make_Moded_Global_List;
-----------------
-- Make_Aspect --
-----------------
function Make_Aspect
(Aspect_Mark : Name_Id;
Aspect_Definition : Node_Id := No_Node) return Node_Id
is
N : Node_Id;
begin
N := New_Node (ADN.K_Aspect);
Set_Aspect_Mark (N, Aspect_Mark);
Set_Aspect_Definition (N, Aspect_Definition);
return N;
end Make_Aspect;
------------------------------
-- Make_Initialization_Spec --
------------------------------
function Make_Initialization_Spec
(Initialization_List : List_Id) return Node_Id
is
N : Node_Id;
begin
N := New_Node (ADN.K_Initialization_Spec);
Set_Initialization_List (N, Initialization_List);
return N;
end Make_Initialization_Spec;
------------------------------
-- Make_Abstract_State_List --
------------------------------
function Make_Abstract_State_List
(State_Name_With_Option : List_Id) return Node_Id
is
N : Node_Id;
begin
N := New_Node (ADN.K_Abstract_State_List);
Set_State_Name_With_Option (N, State_Name_With_Option);
return N;
end Make_Abstract_State_List;
---------------------------------
-- Make_State_Name_With_Option --
---------------------------------
function Make_State_Name_With_Option
(Defining_Identifier : Node_Id;
Synchronous : Boolean;
External : Boolean) return Node_Id
is
N : Node_Id;
begin
N := New_Node (ADN.K_State_Name_With_Option);
Set_Defining_Identifier (N, Defining_Identifier);
Set_Synchronous (N, Synchronous);
Set_External (N, External);
return N;
end Make_State_Name_With_Option;
--------------------------
-- Make_Refinement_List --
--------------------------
function Make_Refinement_List
(Refinement_Clause : List_Id) return Node_Id
is
N : Node_Id;
begin
N := New_Node (Adn.K_Refinement_List);
Set_Refinement_Clause (N, Refinement_Clause);
return N;
end Make_Refinement_List;
----------------------------
-- Make_Refinement_Clause --
----------------------------
function Make_Refinement_Clause
(State_Name : Node_Id;
Constituent : List_Id) return Node_Id
is
N : Node_Id;
begin
N := New_Node (Adn.K_Refinement_Clause);
Set_State_Name (N, State_Name);
Set_Constituent (N, Constituent);
return N;
end Make_Refinement_Clause;
-------------------------------
-- Make_Assignment_Statement --
-------------------------------
......@@ -1257,12 +1406,19 @@ package body Ocarina.Backends.Ada_Tree.Nutils is
-- Make_Defining_Identifier --
------------------------------
function Make_Defining_Identifier (Name : Name_Id) return Node_Id is
function Make_Defining_Identifier
(Name : Name_Id; Normalize : Boolean := True) return Node_Id
is
N : Node_Id;
begin
N := New_Node (K_Defining_Identifier);
Set_Name (N, To_Ada_Name (Name));
if Normalize then
Set_Name (N, To_Ada_Name (Name));
else
Set_Name (N, Name);
end if;
return N;
end Make_Defining_Identifier;
......@@ -2099,15 +2255,21 @@ package body Ocarina.Backends.Ada_Tree.Nutils is
------------------------------------
function Make_Subprogram_Implementation
(Specification : Node_Id;
Declarations : List_Id;
Statements : List_Id) return Node_Id
(Specification : Node_Id;
Declarations : List_Id;
Statements : List_Id;
Aspect_Specification : Node_Id := No_Node) return Node_Id
is
N : Node_Id;
begin
N := New_Node (K_Subprogram_Implementation);
Set_Specification (N, Specification);
if Present (Aspect_Specification) then
Set_Aspect_Specification (ADN.Specification (N),
Aspect_Specification);
end if;
Set_Declarations (N, Declarations);
Set_Statements (N, Statements);
return N;
......@@ -2121,6 +2283,7 @@ package body Ocarina.Backends.Ada_Tree.Nutils is
(Defining_Identifier : Node_Id;
Parameter_Profile : List_Id;
Return_Type : Node_Id := No_Node;
Aspect_Specification : Node_Id := No_Node;
Parent : Node_Id := Current_Package;
Renamed_Subprogram : Node_Id := No_Node;
Instantiated_Subprogram : Node_Id := No_Node) return Node_Id
......@@ -2131,6 +2294,7 @@ package body Ocarina.Backends.Ada_Tree.Nutils is
Set_Defining_Identifier (N, Defining_Identifier);
Set_Parameter_Profile (N, Parameter_Profile);
Set_Return_Type (N, Return_Type);
Set_Aspect_Specification (N, Aspect_Specification);
Set_Parent (N, Parent);
Set_Renamed_Entity (N, Renamed_Subprogram);
Set_Instantiated_Entity (N, Instantiated_Subprogram);
......
src/backends/ast_ada/ocarina-backends-ada_tree-nutils.ads
View file @ 92057e35
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2016 ESA & ISAE. --
-- Copyright (C) 2006-2009 Telecom ParisTech, 2010-2018 ESA & ISAE. --
-- --
-- Ocarina is free software; you can redistribute it and/or modify under --
-- terms of the GNU General Public License as published by the Free Soft- --
......@@ -42,9 +42,9 @@ package Ocarina.Backends.Ada_Tree.Nutils is
type Token_Type is
(
-- Token name Token type
-- Keywords
Tok_Mod, -- MOD **** First Keyword
-- Token name Token type
-- Keywords
Tok_Mod, -- MOD **** First Keyword
Tok_Rem, -- REM
Tok_New, -- NEW
Tok_Abs, -- ABS
......@@ -118,7 +118,7 @@ package Ocarina.Backends.Ada_Tree.Nutils is
Tok_With, -- WITH
Tok_Separate, -- SEPARATE **** Last Keyword
-- Graphic Characters
-- Graphic Characters
Tok_Double_Asterisk, -- **
Tok_Ampersand, -- &
Tok_Minus, -- -
......@@ -146,8 +146,7 @@ package Ocarina.Backends.Ada_Tree.Nutils is
Tok_Vertical_Bar, -- |
Tok_Dot_Dot, -- ..
Tok_Minus_Minus -- --
);
);
Token_Image : array (Token_Type) of Name_Id;
......@@ -204,6 +203,7 @@ package Ocarina.Backends.Ada_Tree.Nutils is
P_Dispatch_Offset,
P_E_Req,
P_Elaboration_Check,
P_Elaborated_Variables,
P_Entity,
P_Entity_Table,
P_Entity_Image,
......@@ -431,6 +431,18 @@ package Ocarina.Backends.Ada_Tree.Nutils is
EN : array (Error_Id) of Name_Id;
type Aspect_Id is
(A_Abstract_State,
A_Global,
A_Initializes,
A_Pre,
A_Refined_Global,
A_Refined_State,
A_Volatile_Function
);
ASN : array (Aspect_Id) of Name_Id;
procedure Add_With_Package
(E : Node_Id;
Used : Boolean := False;
......@@ -514,6 +526,40 @@ package Ocarina.Backends.Ada_Tree.Nutils is
Aliased_Present : Boolean := False) return Node_Id;
-- Usually used with Make_Full_Type_Declaration
function Make_Aspect_Specification
(Aspects : List_Id) return Node_Id;
function Make_Aspect
(Aspect_Mark : Name_Id;
Aspect_Definition : Node_Id := No_Node) return Node_Id;
function Make_Pre
(Subprogram_Call : Node_Id) return Node_Id;
function Make_Global_Specification
(Moded_Global_List : List_Id) return Node_Id;
function Make_Moded_Global_List
(Mode : Mode_Id; Identifier : Node_Id) return Node_Id;
function Make_Initialization_Spec
(Initialization_List : List_Id) return Node_Id;
function Make_Abstract_State_List
(State_Name_With_Option : List_Id) return Node_Id;
function Make_State_Name_With_Option
(Defining_Identifier : Node_Id;
Synchronous : Boolean;
External : Boolean) return Node_Id;
function Make_Refinement_List
(Refinement_Clause : List_Id) return Node_Id;
function Make_Refinement_Clause
(State_Name : Node_Id;
Constituent : List_Id) return Node_Id;
function Make_Assignment_Statement
(Variable_Identifier : Node_Id;
Expression : Node_Id) return Node_Id;
......@@ -557,7 +603,8 @@ package Ocarina.Backends.Ada_Tree.Nutils is
(D_Digits : Unsigned_Long_Long;
D_Scale : Unsigned_Long_Long) return Node_Id;
function Make_Defining_Identifier (Name : Name_Id) return Node_Id;
function Make_Defining_Identifier
(Name : Name_Id; Normalize : Boolean := True) return Node_Id;
function Make_Delay_Statement
(Expression : Node_Id;
......@@ -728,14 +775,16 @@ package Ocarina.Backends.Ada_Tree.Nutils is
Selector_Name : Node_Id) return Node_Id;
function Make_Subprogram_Implementation
(Specification : Node_Id;
Declarations : List_Id;
Statements : List_Id) return Node_Id;
(Specification : Node_Id;
Declarations : List_Id;
Statements : List_Id;
Aspect_Specification : Node_Id := No_Node) return Node_Id;
function Make_Subprogram_Specification
(Defining_Identifier : Node_Id;
Parameter_Profile : List_Id;
Return_Type : Node_Id := No_Node;
Aspect_Specification : Node_Id := No_Node;
Parent : Node_Id := Current_Package;
Renamed_Subprogram : Node_Id := No_Node;
Instantiated_Subprogram : Node_Id := No_Node) return Node_Id;
......
src/backends/ocarina-backends-ada_tree-nodes.idl
View file @ 92057e35
......@@ -125,6 +125,7 @@ module Ocarina::Backends::Ada_Tree::Nodes {
interface Package_Specification : Node_Id {
Node_Id Package_Declaration;
List_Id Withed_Packages;
Node_Id Aspect_Specification;
List_Id Visible_Part;
List_Id Private_Part;
boolean Is_Runtime_Package;
......@@ -137,6 +138,7 @@ module Ocarina::Backends::Ada_Tree::Nodes {
interface Package_Implementation : Node_Id {
Node_Id Package_Declaration;
List_Id Withed_Packages;
Node_Id Aspect_Specification;
List_Id Declarations;
List_Id Statements;
List_Id Package_Initialization;
......@@ -159,6 +161,145 @@ module Ocarina::Backends::Ada_Tree::Nodes {
Name_Id File_Name;
};
/**********/
/* Aspect */
/**********/
/* Ada 2012 Aspect, see Ada RM 13.1.1
aspect_specification ::=
with aspect_mark [=>