Commit a51271c0 authored by yoogx's avatar yoogx

* Use Ada 2012 pre conditions

        For openaadl/ocarina#129
parent de5bd6f5
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2010-2017 ESA & ISAE. --
-- Copyright (C) 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- --
......@@ -33,15 +33,10 @@ with GNAT.OS_Lib; use GNAT.OS_Lib;
with Ocarina.Namet; use Ocarina.Namet;
with Utils; use Utils;
with Ocarina.ME_AADL.AADL_Instances.Nodes;
with Ocarina.ME_AADL.AADL_Instances.Nutils;
with Ocarina.ME_AADL.AADL_Instances.Entities;
with Ocarina.Backends.Build_Utils;
with Ocarina.Backends.Helper;
with Ocarina.Backends.Messages;
with Ocarina.Backends.Properties;
with Ocarina.Backends.Utils;
with Ocarina.Backends.XML_Common.Mapping;
with Ocarina.Backends.XML_Tree.Nodes;
with Ocarina.Backends.XML_Tree.Nutils;
......@@ -49,21 +44,15 @@ with Ocarina.Backends.XML_Values;
package body Ocarina.Backends.Cheddar.Mapping is
use Ocarina.ME_AADL;
use Ocarina.ME_AADL.AADL_Instances.Nodes;
use Ocarina.ME_AADL.AADL_Instances.Entities;
use Ocarina.Backends.Helper;
use Ocarina.Backends.Build_Utils;
use Ocarina.Backends.Messages;
use Ocarina.Backends.Properties;
use Ocarina.Backends.Utils;
use Ocarina.Backends.XML_Common.Mapping;
use Ocarina.Backends.XML_Tree.Nodes;
use Ocarina.Backends.XML_Tree.Nutils;
package AIN renames Ocarina.ME_AADL.AADL_Instances.Nodes;
package AINU renames Ocarina.ME_AADL.AADL_Instances.Nutils;
-- package AIN renames Ocarina.ME_AADL.AADL_Instances.Nodes;
package XTN renames Ocarina.Backends.XML_Tree.Nodes;
package XV renames Ocarina.Backends.XML_Values;
......
------------------------------------------------------------------------------
-- --
-- OCARINA COMPONENTS --
......@@ -6,7 +7,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2010-2015 ESA & ISAE. --
-- Copyright (C) 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- --
......@@ -29,15 +30,122 @@
-- --
------------------------------------------------------------------------------
with Ocarina.ME_AADL;
with Ocarina.ME_AADL.AADL_Instances.Nutils;
with Ocarina.ME_AADL.AADL_Instances.Nodes;
with Ocarina.Backends.Properties;
with Ocarina.Backends.Helper;
with Ocarina.Backends.Utils;
package Ocarina.Backends.Cheddar.Mapping is
use Ocarina.ME_AADL;
use Ocarina.ME_AADL.AADL_Instances.Nodes;
use Ocarina.Backends.Properties;
use Ocarina.Backends.Helper;
use Ocarina.Backends.Utils;
package AIN renames Ocarina.ME_AADL.AADL_Instances.Nodes;
package AINU renames Ocarina.ME_AADL.AADL_Instances.Nutils;
function Map_HI_Node (E : Node_Id) return Node_Id;
function Map_HI_Unit (E : Node_Id) return Node_Id;
function Map_Processor (E : Node_Id) return Node_Id;
function Map_Process (E : Node_Id) return Node_Id;
function Map_Thread (E : Node_Id) return Node_Id;
function Map_Buffer (E : Node_Id; P : Node_Id) return Node_Id;
function Map_Processor (E : Node_Id) return Node_Id with
Pre => (True and then
-- 1/ Typing
AINU.Is_Processor (E) and then
-- 2/ Property requirements
-- a) Scheduling_Protocol policy is specified
(Get_Scheduling_Protocol (E) /= Unknown_Scheduler)
);
function Map_Process (E : Node_Id) return Node_Id with
Pre => (
-- 1/ Typing
AINU.Is_Process (E)
);
function Map_Thread (E : Node_Id) return Node_Id with
Pre => (True and then
-- 1/ Typing
AINU.Is_Thread (E) and then
-- 2/ Property requirements
-- The thread is a) periodic, b) has
-- compute_execution_time specified, is either
-- periodic or sporadic, and has a period
(Get_Thread_Dispatch_Protocol (E) /= Thread_None) and then
(Get_Execution_Time (E) /= Empty_Time_Array) and then
(if Get_Thread_Dispatch_Protocol (E) = Thread_Periodic or else
Get_Thread_Dispatch_Protocol (E) = Thread_Periodic then
Get_Thread_Period (E) /= Null_Time) and then
-- 3/ Architecture requirements
-- a) There is a linked processor P for E
(for some P of Processors (Get_Root_Component (E)) =>
AINU.Is_Processor (P) and then
P = Get_Bound_Processor
(Corresponding_Instance
(Get_Container_Process (Parent_Subcomponent (E)))))
);
function Map_Data (E : Node_Id) return Node_Id with
Pre => (True and then
-- 1/ Typing
AINU.Is_Data (E) and then
-- 2/ Architecture requirements
-- a) There is a linked processor P for E
(for some P of Processors (Get_Root_Component (E)) =>
AINU.Is_Processor (P) and then
P = Get_Bound_Processor
(Corresponding_Instance
(Get_Container_Process (Parent_Subcomponent (E)))))
and then
-- b) There is at least one thread accessing the data
(for some T of Threads (Get_Root_Component (E)) =>
(for some C of Connections_Of
(Corresponding_Instance
(Get_Container_Process
(Parent_Subcomponent (E))))
=> T = Corresponding_Instance
(Item (AIN.First_Node
(Path (Destination (C)))))))
);
function Map_Buffer (E : Node_Id; P : Node_Id) return Node_Id with
Pre => (True and then
-- 1/ Typing
-- a) E is a thread
AINU.Is_Thread (E) and then
-- b) P is an in event (data) port of E
AINU.Is_Port (P) and then
Is_Event (P) and then
Is_In (P) and then
(for some F of Features_Of (E) => P = F) and then
-- 2/ Architecture requirements
-- a) There is a linked processor P for E
(for some CPU of Processors (Get_Root_Component (E)) =>
AINU.Is_Processor (CPU) and then
CPU = Get_Bound_Processor
(Corresponding_Instance
(Get_Container_Process (Parent_Subcomponent (E)))))
and then
-- b) P is connected to some threads
not AINU.Is_Empty (Get_Source_Ports (P))
);
function Map_Dependency (E : Node_Id; P : Node_Id) return Node_Id;
function Map_Data (E : Node_Id) return Node_Id;
end Ocarina.Backends.Cheddar.Mapping;
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