Skip to content

GitLab

Commit 44101084 authored by yoogx's avatar yoogx
Browse files

* Remove obsolete platforms 

	For openaadl/ocarina#161
parent c95a970c
Hide whitespace changes
Inline Side-by-side
resources/deployment.aadl
View file @ 44101084
......@@ -28,18 +28,12 @@ property set Deployment is
LEON3_SCOC3, -- LEON3 with RTEMS for SCOC3
LEON3_XTRATUM, -- LEON3 with Xtratum
LEON3_XM3, -- RTEMS for XTRATUM/LEON3
LEON_ORK, -- LEON2 board or tsim-leon (ORK)
LEON_GNAT, -- LEON2 board or qemu (GNATPRO/HI-E)
LINUX32, -- Linux 32 bits
LINUX32_XENOMAI_NATIVE, -- Linux 32 bits with native Xenomai
LINUX32_XENOMAI_POSIX, -- Linux 32 bits with Xenomai and POSIX skin
LINUX64, -- Linux 64 bits
ERC32_ORK, -- ERC32 board or tsim-erc32 (ORK)
ARM_DSLINUX, -- Nintendo DS (tm) (DSLinux)
ARM_N770, -- Nokia N770 (tm)
GUMSTIX_RTEMS, -- Gumstix under RTEMS
NDS_RTEMS, -- Nintendo DS under RTEMS
X86_RTEMS, -- x86 under RTEMS
X86_RTEMS_POSIX, -- x86 under RTEMS with POSIX layer
X86_LINUXTASTE, -- TASTE-specific linux distribution
MARTE_OS, -- MaRTE OS
......
src/backends/ocarina-backends-properties.adb
View file @ 44101084
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2017 ESA & ISAE. --
-- Copyright (C) 2008-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- --
......@@ -317,23 +317,15 @@ package body Ocarina.Backends.Properties is
Platform_LINUX32_Xenomai_Native_Name : Name_Id;
Platform_LINUX32_Xenomai_Posix_Name : Name_Id;
Platform_LINUX64_Name : Name_Id;
Platform_NDS_RTEMS_Name : Name_Id;
Platform_NDS_RTEMS_POSIX_Name : Name_Id;
Platform_Gumstix_RTEMS_Name : Name_Id;
Platform_Gumstix_RTEMS_POSIX_Name : Name_Id;
Platform_LEON_RTEMS_Name : Name_Id;
Platform_LEON_RTEMS_POSIX_Name : Name_Id;
Platform_X86_LINUXTASTE_Name : Name_Id;
Platform_X86_RTEMS_Name : Name_Id;
Platform_X86_RTEMS_POSIX_Name : Name_Id;
Platform_LEON_GNAT_Name : Name_Id;
Platform_LEON_ORK_Name : Name_Id;
Platform_LEON3_SCOC3_Name : Name_Id;
Platform_LEON3_XM3_Name : Name_Id;
Platform_LEON3_Xtratum_Name : Name_Id;
Platform_ERC32_ORK_Name : Name_Id;
Platform_ARM_DSLINUX_Name : Name_Id;
Platform_ARM_N770_Name : Name_Id;
Platform_MARTE_OS_Name : Name_Id;
Platform_Vxworks_Name : Name_Id;
Platform_GNAT_Runtime_Name : Name_Id;
......@@ -2431,14 +2423,6 @@ package body Ocarina.Backends.Properties is
return Platform_Bench;
elsif P_Name = Platform_Native_Compcert_Name then
return Platform_Native_Compcert;
elsif P_Name = Platform_Gumstix_RTEMS_POSIX_Name then
return Platform_Gumstix_RTEMS_POSIX;
elsif P_Name = Platform_Gumstix_RTEMS_Name then
return Platform_Gumstix_RTEMS;
elsif P_Name = Platform_NDS_RTEMS_POSIX_Name then
return Platform_NDS_RTEMS_POSIX;
elsif P_Name = Platform_NDS_RTEMS_Name then
return Platform_NDS_RTEMS;
elsif P_Name = Platform_LEON_RTEMS_POSIX_Name then
return Platform_LEON_RTEMS_POSIX;
elsif P_Name = Platform_LEON_RTEMS_Name then
......@@ -2455,10 +2439,6 @@ package body Ocarina.Backends.Properties is
return Platform_LINUX32_XENOMAI_POSIX;
elsif P_Name = Platform_LINUX64_Name then
return Platform_LINUX64;
elsif P_Name = Platform_X86_RTEMS_POSIX_Name then
return Platform_X86_RTEMS_POSIX;
elsif P_Name = Platform_X86_RTEMS_Name then
return Platform_X86_RTEMS;
elsif P_Name = Platform_LEON_GNAT_Name then
return Platform_LEON_GNAT;
elsif P_Name = Platform_LEON_ORK_Name then
......@@ -2471,10 +2451,6 @@ package body Ocarina.Backends.Properties is
return Platform_LEON3_XTRATUM;
elsif P_Name = Platform_ERC32_ORK_Name then
return Platform_ERC32_ORK;
elsif P_Name = Platform_ARM_DSLINUX_Name then
return Platform_ARM_DSLINUX;
elsif P_Name = Platform_ARM_N770_Name then
return Platform_ARM_N770;
elsif P_Name = Platform_MARTE_OS_Name then
return Platform_MARTE_OS;
elsif P_Name = Platform_Vxworks_Name then
......@@ -3024,15 +3000,6 @@ package body Ocarina.Backends.Properties is
Platform_Native_Name := Get_String_Name ("native");
Platform_Bench_Name := Get_String_Name ("bench");
Platform_Native_Compcert_Name := Get_String_Name ("native_compcert");
Platform_Gumstix_RTEMS_Name := Get_String_Name ("gumstix_rtems");
Platform_Gumstix_RTEMS_POSIX_Name :=
Get_String_Name ("gumstix_rtems_posix");
Platform_NDS_RTEMS_Name := Get_String_Name ("nds_rtems");
Platform_NDS_RTEMS_POSIX_Name := Get_String_Name ("nds_rtems_posix");
Platform_X86_RTEMS_Name := Get_String_Name ("x86_rtems");
Platform_X86_RTEMS_POSIX_Name := Get_String_Name ("x86_rtems_posix");
Platform_LINUX32_Name := Get_String_Name ("linux32");
Platform_Win32_Name := Get_String_Name ("win32");
Platform_LINUX32_Xenomai_Native_Name :=
......@@ -3049,8 +3016,6 @@ package body Ocarina.Backends.Properties is
Platform_LEON3_XM3_Name := Get_String_Name ("leon3_xm3");
Platform_LEON3_Xtratum_Name := Get_String_Name ("leon3_xtratum");
Platform_ERC32_ORK_Name := Get_String_Name ("erc32_ork");
Platform_ARM_DSLINUX_Name := Get_String_Name ("arm_dslinux");
Platform_ARM_N770_Name := Get_String_Name ("arm_n770");
Platform_MARTE_OS_Name := Get_String_Name ("marte_os");
Platform_Vxworks_Name := Get_String_Name ("vxworks");
Platform_GNAT_Runtime_Name := Get_String_Name ("gnat_runtime");
......
src/backends/ocarina-backends-properties.ads
View file @ 44101084
......@@ -6,7 +6,7 @@
-- --
-- S p e c --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2017 ESA & ISAE. --
-- Copyright (C) 2008-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- --
......@@ -543,15 +543,9 @@ package Ocarina.Backends.Properties is
(Platform_Native,
Platform_Native_Compcert,
Platform_Bench,
Platform_Gumstix_RTEMS,
Platform_Gumstix_RTEMS_POSIX,
Platform_NDS_RTEMS,
Platform_NDS_RTEMS_POSIX,
Platform_X86_LINUXTASTE,
Platform_LEON_RTEMS,
Platform_LEON_RTEMS_POSIX,
Platform_X86_RTEMS,
Platform_X86_RTEMS_POSIX,
Platform_X86_LINUXTASTE,
Platform_LEON_GNAT,
Platform_LEON3_SCOC3,
Platform_LEON3_XM3,
......@@ -563,8 +557,6 @@ package Ocarina.Backends.Properties is
Platform_LINUX32_XENOMAI_POSIX,
Platform_LINUX64,
Platform_ERC32_ORK,
Platform_ARM_DSLINUX,
Platform_ARM_N770,
Platform_MARTE_OS,
Platform_VxWorks,
Platform_GNAT_Runtime,
......
src/backends/po_hi_c/ocarina-backends-po_hi_c-deployment.adb
View file @ 44101084
......@@ -2262,8 +2262,6 @@ package body Ocarina.Backends.PO_HI_C.Deployment is
case Execution_Platform is
when Platform_Native |
Platform_None |
Platform_X86_RTEMS |
Platform_X86_RTEMS_POSIX |
Platform_LINUX32_XENOMAI_NATIVE |
Platform_Native_Compcert |
Platform_LINUX32_XENOMAI_POSIX |
......@@ -2277,12 +2275,6 @@ package body Ocarina.Backends.PO_HI_C.Deployment is
when Platform_LEON_RTEMS |
Platform_LEON_RTEMS_POSIX |
Platform_LEON_ORK |
Platform_ARM_DSLINUX |
Platform_ARM_N770 |
Platform_NDS_RTEMS |
Platform_NDS_RTEMS_POSIX |
Platform_Gumstix_RTEMS |
Platform_Gumstix_RTEMS_POSIX |
Platform_LEON3_XM3 =>
Append_Node_To_List
(RE (RE_Bigendian),
......
src/backends/po_hi_c/ocarina-backends-po_hi_c.adb
View file @ 44101084
......@@ -6,7 +6,7 @@
-- --
-- B o d y --
-- --
-- Copyright (C) 2008-2009 Telecom ParisTech, 2010-2016 ESA & ISAE. --
-- Copyright (C) 2008-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- --
......@@ -209,18 +209,6 @@ package body Ocarina.Backends.PO_HI_C is
when Platform_Native_Compcert =>
Write_Str ("compcert");
when Platform_NDS_RTEMS =>
Write_Str ("nds.rtems");
when Platform_NDS_RTEMS_POSIX =>
Write_Str ("nds.rtems_posix");
when Platform_Gumstix_RTEMS =>
Write_Str ("gumstix.rtems");
when Platform_Gumstix_RTEMS_POSIX =>
Write_Str ("gumstix.rtems_posix");
when Platform_Bench =>
Write_Str ("bench");
......@@ -233,18 +221,6 @@ package body Ocarina.Backends.PO_HI_C is
when Platform_X86_LINUXTASTE =>
Write_Str ("x86.linuxtaste");
when Platform_X86_RTEMS =>
Write_Str ("x86.rtems");
when Platform_X86_RTEMS_POSIX =>
Write_Str ("x86.rtems_posix");
when Platform_ARM_DSLINUX =>
Write_Str ("arm.dslinux");
when Platform_ARM_N770 =>
Write_Str ("arm.n770");
when Platform_LINUX64 =>
Write_Str ("linux64");
......
tests/real-annexes-execution/test_real_exec_02.aadl.out
View file @ 44101084
......@@ -151,22 +151,22 @@ Evaluating theorem set_declaration_is_passing_through
* Iterate for variable: rma.erc32_node_a_task_1
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :4014 end to end flow spec
anonymous end to end flow :4024 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_2
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :4014 end to end flow spec
anonymous end to end flow :4024 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_12
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :4015 end to end flow spec
anonymous end to end flow :4025 end to end flow spec
=> Result: TRUE
* Iterate for variable: rma.erc32_node_a_task_22
Content of set accessor_flows (test_real_exec_02.aadl:251:21) is
anonymous end to end flow :4015 end to end flow spec
anonymous end to end flow :4025 end to end flow spec
=> Result: TRUE
theorem set_declaration_is_passing_through is: TRUE
......
tests/real-annexes-parsing/test_real_parse_01.aadl.out
View file @ 44101084
......@@ -78,7 +78,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type
applies to (system);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_CORTEX, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Execution_Platform : Deployment::Allowed_Execution_Platform
applies to ( all);
......@@ -685,10 +685,10 @@ system)
applies to (system);
dataview : list of aadlstring
applies to (package);
applies to (package, system);
dataviewpath : list of aadlstring
applies to (package);
applies to (package, system);
Encoding_type : type enumeration (native, uper, acn);
......
tests/real-annexes-parsing/test_real_parse_02.aadl.out
View file @ 44101084
......@@ -78,7 +78,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type
applies to (system);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_CORTEX, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Execution_Platform : Deployment::Allowed_Execution_Platform
applies to ( all);
......@@ -685,10 +685,10 @@ system)
applies to (system);
dataview : list of aadlstring
applies to (package);
applies to (package, system);
dataviewpath : list of aadlstring
applies to (package);
applies to (package, system);
Encoding_type : type enumeration (native, uper, acn);
......
tests/real-annexes-parsing/test_real_parse_03.aadl.out
View file @ 44101084
......@@ -78,7 +78,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type
applies to (system);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_CORTEX, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Execution_Platform : Deployment::Allowed_Execution_Platform
applies to ( all);
......@@ -685,10 +685,10 @@ system)
applies to (system);
dataview : list of aadlstring
applies to (package);
applies to (package, system);
dataviewpath : list of aadlstring
applies to (package);
applies to (package, system);
Encoding_type : type enumeration (native, uper, acn);
......
tests/real-annexes-parsing/test_real_parse_04.aadl.out
View file @ 44101084
......@@ -78,7 +78,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type
applies to (system);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_CORTEX, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Execution_Platform : Deployment::Allowed_Execution_Platform
applies to ( all);
......@@ -685,10 +685,10 @@ system)
applies to (system);
dataview : list of aadlstring
applies to (package);
applies to (package, system);
dataviewpath : list of aadlstring
applies to (package);
applies to (package, system);
Encoding_type : type enumeration (native, uper, acn);
......
tests/real-annexes-parsing/test_real_parse_05.aadl.out
View file @ 44101084
......@@ -78,7 +78,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type
applies to (system);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_CORTEX, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Execution_Platform : Deployment::Allowed_Execution_Platform
applies to ( all);
......@@ -685,10 +685,10 @@ system)
applies to (system);
dataview : list of aadlstring
applies to (package);
applies to (package, system);
dataviewpath : list of aadlstring
applies to (package);
applies to (package, system);
Encoding_type : type enumeration (native, uper, acn);
......
tests/test042/test.aadl.out
View file @ 44101084
......@@ -74,7 +74,7 @@ property set Deployment is
Protocol : Deployment::Protocol_Type
applies to (system);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Allowed_Execution_Platform : type enumeration (Native, Native_Compcert, bench, GNAT_Runtime, LEON_RTEMS, LEON_RTEMS_POSIX, LEON3_SCOC3, LEON3_XTRATUM, LEON3_XM3, LEON_ORK, LEON_GNAT, LINUX32, LINUX32_XENOMAI_NATIVE, LINUX32_XENOMAI_POSIX, LINUX64, ERC32_ORK, ARM_CORTEX, ARM_DSLINUX, ARM_N770, GUMSTIX_RTEMS, NDS_RTEMS, X86_RTEMS, X86_RTEMS_POSIX, X86_LINUXTASTE, MARTE_OS, WIN32, VXWORKS, FREERTOS);
Execution_Platform : Deployment::Allowed_Execution_Platform
applies to ( all);
......@@ -681,10 +681,10 @@ system)
applies to (system);
dataview : list of aadlstring
applies to (package);
applies to (package, system);
dataviewpath : list of aadlstring
applies to (package);
applies to (package, system);
Encoding_type : type enumeration (native, uper, acn);
......
tests/test_tree_p2/test.aadl.out
View file @ 44101084
This source diff could not be displayed because it is too large. You can view the blob instead.
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