Merge https://github.com/openaadl/ocarina

.travis.yml

@@ -19,7 +19,7 @@ osx_image: xcode8.3
 env:
   global:
     - TOOLS_DIR=$HOME/build_tools
-    - GNAT_TAR_PATH=$TOOLS_DIR/gnat-gpl-2016-bin.tar.gz
+    - INSTALL_DIR=$HOME/tools
 
 ################################################################################
 # Host to run the various tests
@@ -36,25 +36,19 @@ os:
 cache:
   directories:
   - $HOME/build_tools
+  - $HOME/tools
 
 # 2/ Check Python installation
 
 before_install:
 - which python
 
-# 3/ Install GNAT GPL 2016
+# 3/ Install GNAT
 
 install:
-  # Check if the GNAT package is already available in the cache directory. If
-  # not, download it.
-  - if [[ "$TRAVIS_OS_NAME" == "linux" ]]; then test -f  $GNAT_TAR_PATH ||( mkdir -p $TOOLS_DIR && wget http://mirrors.cdn.adacore.com/art/5739cefdc7a447658e0b016b -O $GNAT_TAR_PATH); fi
-  - if [[ "$TRAVIS_OS_NAME" == "osx" ]]; then test -f  $GNAT_TAR_PATH ||( mkdir -p $TOOLS_DIR && wget http://mirrors.cdn.adacore.com/art/573a396cc7a447658d00e430 -O $GNAT_TAR_PATH); fi
-
-  # Extract GNAT from its package
-  - tar -xf $GNAT_TAR_PATH
-
-  # Add GNAT to $PATH
-  - export PATH=$PWD/gnat-gpl-2016-x86_64-linux-bin/bin/:$PWD/gnat-gpl-2016-x86_64-darwin-bin/bin/:$PATH
+  - git clone https://github.com/OpenAADL/ocarina-build.git ; ( cd ocarina-build ; ./build_ocarina.sh --install-gnat-ce ; cd $HOME)
+  - export PATH=$HOME/tools/bin:$PATH
+  - echo $PATH
 
 ################################################################################
 # Main processing starts here
@@ -65,7 +59,7 @@ script:
   - gnatls -v
 
   # Just build
-  - git clone https://github.com/OpenAADL/ocarina-build.git ; ( cd ocarina-build ; ./build_ocarina.sh --scenario=travis-ci )
+  - ( cd ocarina-build ; ./build_ocarina.sh --scenario=travis-ci )
 
 # Codecov.io
 after_success:

src/backends/po_hi_ada/ocarina-backends-po_hi_ada-activity.adb

@@ -197,7 +197,22 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
 
    function Get_Value_Spec (E : Node_Id) return Node_Id is
       N : Node_Id;
+      Aspect_Node : Node_Id := No_Node;
    begin
+      if Add_SPARK2014_Annotations then
+         Aspect_Node := 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))))))));
+
+      end if;
+
       N :=
         Make_Subprogram_Specification
           (Defining_Identifier => Make_Defining_Identifier (SN (S_Get_Value)),
@@ -214,14 +229,15 @@ package body Ocarina.Backends.PO_HI_Ada.Activity is
                    Subtype_Mark =>
                      Make_Defining_Identifier (Map_Port_Enumeration_Name (E)),
                    Parameter_Mode => Mode_In),
-                Make_Parameter_Specification
-                  (Defining_Identifier =>
-                     Make_Defining_Identifier (PN (P_Result)),
-                   Subtype_Mark =>
-                     Make_Defining_Identifier (Map_Port_Interface_Name (E)),
-                   Parameter_Mode => Mode_Inout)
+                   Make_Parameter_Specification
+                     (Defining_Identifier =>
+                        Make_Defining_Identifier (PN (P_Result)),
+                      Subtype_Mark =>
+                        Make_Defining_Identifier (Map_Port_Interface_Name (E)),
+                      Parameter_Mode => Mode_Inout)
                ),
-           Aspect_Specification => Runtime_Spec_Aspect_Definition);
+           Aspect_Specification => Aspect_Node);
+
       return N;
    end Get_Value_Spec;
 
@@ -1908,12 +1924,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);

src/backends/po_hi_ada/ocarina-backends-po_hi_ada-job.adb

@@ -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 --
       -------------------
@@ -2807,24 +2778,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);
@@ -2844,7 +2797,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
 
@@ -2937,10 +2889,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;

src/backends/po_hi_ada/ocarina-backends-po_hi_ada.adb

@@ -501,9 +501,15 @@ package body Ocarina.Backends.PO_HI_Ada is
       case Transport_API is
          when Transport_BSD_Sockets =>
             Write_Indentation;
-            Write_Line
-              ("for Body (""PolyORB_HI.Transport_Low_Level"")" &
-               " use ""polyorb_hi-transport_low_level_sockets.adb"";");
+            if Add_SPARK2014_Annotations then
+               Write_Line
+                 ("for Body (""PolyORB_HI.Transport_Low_Level"")" &
+                    " use ""polyorb_hi-transport_low_level_spark.adb"";");
+            else
+               Write_Line
+                 ("for Body (""PolyORB_HI.Transport_Low_Level"")" &
+                    " use ""polyorb_hi-transport_low_level_sockets.adb"";");
+            end if;
 
          when Transport_SpaceWire =>
             raise Program_Error;

src/core/instance/ocarina-instances.adb

@@ -222,7 +222,7 @@ package body Ocarina.Instances is
 
          if No (Root_System) then
             Error_Loc (1) := No_Location;
-            DE ("Cannot find a root system");
+            Exit_On_Error (True, "Cannot find a root system");
          end if;
 
          if Root_System_Name /= No_Name

support/Makefile.am

 headers_ocarina: headers_ocarina.adb
-	$(GNATMAKE) -gnat05 $(srcdir)/headers_ocarina.adb
+	$(GNATMAKE) $(srcdir)/headers_ocarina.adb
 
 EXTRA_DIST= $(srcdir)/reconfig