Skip to content

GitLab

O
Ocarina
Commit a81aa3d1 authored by yoogx's avatar yoogx
Browse files
Options

* Remove generation of old SPARK annotations

parent d784c7eb
Hide whitespace changes
Inline Side-by-side
Showing with 0 additions and 260 deletions
src/backends/ocarina-backends-ada_tree-generator-spark.adb deleted 100644 → 0
View file @ d784c7eb
------------------------------------------------------------------------------
-- --
-- OCARINA COMPONENTS --
-- --
-- OCARINA.BACKENDS.ADA_TREE.GENERATOR.SPARK --
-- --
-- B o d y --
-- --
-- Copyright (C) 2009 Telecom ParisTech, 2010-2015 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- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. Ocarina is distributed in the hope that it will be useful, but --
-- WITHOUT ANY WARRANTY; without even the implied warranty of --
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
-- --
-- Ocarina is maintained by the TASTE project --
-- (taste-users@lists.tuxfamily.org) --
-- --
------------------------------------------------------------------------------
with Ocarina.Namet; use Ocarina.Namet;
with Ocarina.Output; use Ocarina.Output;
with Ocarina.Backends.Ada_Tree.Nodes;
with Ocarina.Backends.Ada_Tree.Nutils;
with Ocarina.Backends.Ada_Tree.Generator;
package body Ocarina.Backends.Ada_Tree.Generator.Spark is
use Ocarina.Backends.Ada_Tree.Generator;
use Ocarina.Backends.Ada_Tree.Nodes;
use Ocarina.Backends.Ada_Tree.Nutils;
procedure Write (T : Token_Type);
-----------
-- Write --
-----------
procedure Write (T : Token_Type) is
begin
Write_Name (Token_Image (T));
end Write;
----------------------------------
-- Generate_Inherit_Annotations --
----------------------------------
procedure Generate_Inherit_Annotations (N : Node_Id) is
P : Node_Id;
LS : List_Id := No_List;
LB : List_Id := No_List;
begin
-- Initialize withed package lists for a package specification
if Kind (N) = K_Package_Specification then
LS := Withed_Packages (N);
LB :=
Withed_Packages (Package_Implementation (Package_Declaration (N)));
-- Initialize withed package lists for a subprogram specification
elsif Kind (N) = K_Subprogram_Specification then
LS := Withed_Packages (N);
if Subprogram_Implementation (Main_Subprogram_Unit (N)) /=
No_Node
then
LB :=
Withed_Packages
(Subprogram_Implementation (Main_Subprogram_Unit (N)));
end if;
-- Initialize withed package lists for a subprogram implementation
elsif Kind (N) = K_Subprogram_Implementation then
LS := Withed_Packages (N);
if Subprogram_Specification (Main_Subprogram_Unit (N)) /= No_Node then
LB :=
Withed_Packages
(Subprogram_Specification (Main_Subprogram_Unit (N)));
end if;
end if;
-- inherit clauses for package specification
if not Is_Empty (LS) then
Increment_Indentation;
Write (Tok_Annotation);
Write_Space;
Write (Tok_Inherit);
Write_Space;
P := First_Node (LS);
loop
Generate (Defining_Identifier (P));
P := Next_Node (P);
exit when No (P);
Write (Tok_Comma);
Write_Eol;
Write (Tok_Annotation);
Write_Indentation (7);
end loop;
end if;
-- inherit clauses for package implementation
if Is_Empty (Withed_Packages (N)) and then not Is_Empty (LB) then
Increment_Indentation;
Write (Tok_Annotation);
Write_Space;
Write (Tok_Inherit);
Write_Space;
elsif not Is_Empty (LS) and then not Is_Empty (LB) then
Write (Tok_Comma);
Write_Eol;
Write (Tok_Annotation);
Write_Indentation (7);
end if;
if not Is_Empty (LB) then
P := First_Node (LB);
loop
Generate (Defining_Identifier (P));
P := Next_Node (P);
exit when No (P);
Write (Tok_Comma);
Write_Eol;
Write (Tok_Annotation);
Write_Indentation (7);
end loop;
end if;
if not Is_Empty (LS) or else not Is_Empty (LB) then
Write (Tok_Semicolon);
Write_Eol;
Decrement_Indentation;
end if;
end Generate_Inherit_Annotations;
-----------------------------
-- Generate_Own_Annotation --
-----------------------------
procedure Generate_Own_Annotation (N : Node_Id) is
begin
case Own_Mode (N) is
when Mode_In =>
null;
when Mode_Out =>
Write (Tok_Out);
Write_Space;
when Mode_Inout =>
Write (Tok_In);
Write_Space;
Write (Tok_Out);
Write_Space;
end case;
if Is_Protected (N) then
Write (Tok_Protected);
Write_Space;
end if;
Generate (Variable (N));
end Generate_Own_Annotation;
----------------------------------
-- Generate_Own_Annotation_List --
----------------------------------
procedure Generate_Own_Annotation_List (L : List_Id) is
P : Node_Id;
begin
P := First_Node (L);
Write (Tok_Annotation);
Write_Space;
Write (Tok_Own);
loop
Write_Indentation;
Write_Space;
Generate (P);
P := Next_Node (P);
exit when No (P);
Write (Tok_Semicolon);
Write_Eol;
Write (Tok_Annotation);
end loop;
Write (Tok_Semicolon);
Write_Eol;
end Generate_Own_Annotation_List;
end Ocarina.Backends.Ada_Tree.Generator.Spark;
src/backends/ocarina-backends-ada_tree-generator-spark.ads deleted 100644 → 0
View file @ d784c7eb
------------------------------------------------------------------------------
-- --
-- OCARINA COMPONENTS --
-- --
-- OCARINA.BACKENDS.ADA_TREE.GENERATOR.SPARK --
-- --
-- S p e c --
-- --
-- Copyright (C) 2009 Telecom ParisTech, 2010-2015 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- --
-- ware Foundation; either version 3, or (at your option) any later ver- --
-- sion. Ocarina is distributed in the hope that it will be useful, but --
-- WITHOUT ANY WARRANTY; without even the implied warranty of --
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. --
-- --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception, --
-- version 3.1, as published by the Free Software Foundation. --
-- --
-- You should have received a copy of the GNU General Public License and --
-- a copy of the GCC Runtime Library Exception along with this program; --
-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
-- <http://www.gnu.org/licenses/>. --
-- --
-- Ocarina is maintained by the TASTE project --
-- (taste-users@lists.tuxfamily.org) --
-- --
------------------------------------------------------------------------------
package Ocarina.Backends.Ada_Tree.Generator.Spark is
procedure Generate_Inherit_Annotations (N : Node_Id);
-- Generate inherit clauses annotations for SPARK.
-- The procedure takes as parameter a withed package node.
procedure Generate_Own_Annotation_List (L : List_Id);
-- Generate Own Annotations for SPARK.
-- The procedure takes a list of Own_Annotation nodes
procedure Generate_Own_Annotation (N : Node_Id);
end Ocarina.Backends.Ada_Tree.Generator.Spark;
src/backends/ocarina-backends-ada_tree-generator.adb
View file @ a81aa3d1
......@@ -40,7 +40,6 @@ with Ocarina.Backends.Utils;
with Ocarina.Backends.Ada_Tree.Nodes;
with Ocarina.Backends.Ada_Tree.Nutils;
with Ocarina.Backends.Ada_Values;
with Ocarina.Backends.Ada_Tree.Generator.Spark;
package body Ocarina.Backends.Ada_Tree.Generator is
......@@ -305,9 +304,6 @@ package body Ocarina.Backends.Ada_Tree.Generator is
when K_Object_Declaration =>
Generate_Object_Declaration (N);
when K_SPARK_Own_Annotation =>
Spark.Generate_Own_Annotation (N);
when K_Object_Instantiation =>
Generate_Object_Instantiation (N);
......@@ -1729,9 +1725,6 @@ package body Ocarina.Backends.Ada_Tree.Generator is
end loop;
Write_Eol;
-- Generate inherit annotations for SPARK
Spark.Generate_Inherit_Annotations (N);
if Is_Instantiated_Package (N) then
Generate (Package_Instantiation (N));
Generate_Statement_Delimiter (Package_Instantiation (N));
......@@ -1744,10 +1737,6 @@ package body Ocarina.Backends.Ada_Tree.Generator is
Write (Tok_Is);
Write_Eol (2);
if not Is_Empty (SPARK_Own_Annotations (N)) then
Spark.Generate_Own_Annotation_List (SPARK_Own_Annotations (N));
end if;
Increment_Indentation;
P := First_Node (Visible_Part (N));
while Present (P) loop
......@@ -2251,11 +2240,6 @@ package body Ocarina.Backends.Ada_Tree.Generator is
Write_Indentation;
end if;
-- Generate inherit annotations for SPARK
if Present (Main_Subprogram_Unit (N)) then
Spark.Generate_Inherit_Annotations (N);
end if;
Generate_Comment_Box (Name (Defining_Identifier (P)));
Write_Eol;
......@@ -2351,11 +2335,6 @@ package body Ocarina.Backends.Ada_Tree.Generator is
Write_Indentation;
end if;
-- Generate inherit annotations for SPARK
if Present (Main_Subprogram_Unit (N)) then
Spark.Generate_Inherit_Annotations (N);
end if;
if Present (T) then
Write (Tok_Function);
else
......
Markdown is supported
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