Merge branch 'master' of https://github.com/OpenAADL/ocarina

examples/real/security/all.aadl.out

@@ -5,6 +5,74 @@ all.aadl:195:07: warning: layer_topsecret references a component type
 all.aadl:196:07: warning: layer_secret references a component type
 all.aadl:197:07: warning: layer_unclassified references a component type
 ocarina: Total: 0 error and 6 warnings
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:15:23 Backends: warning : cardinal of set b is null
+lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
+lib.real:117:20 Backends: warning : cardinal of set b_dst is null
+lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:119:20 Backends: warning : cardinal of set b_dst is null
+lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:117:20 Backends: warning : cardinal of set b_dst is null
+lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:119:20 Backends: warning : cardinal of set b_dst is null
+lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:117:20 Backends: warning : cardinal of set b_dst is null
+lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:119:20 Backends: warning : cardinal of set b_dst is null
+lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:117:20 Backends: warning : cardinal of set b_dst is null
+lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:119:20 Backends: warning : cardinal of set b_dst is null
+lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:117:20 Backends: warning : cardinal of set b_dst is null
+lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:119:20 Backends: warning : cardinal of set b_dst is null
+lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:117:20 Backends: warning : cardinal of set b_dst is null
+lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
+lib.real:119:20 Backends: warning : cardinal of set b_dst is null
+lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
+lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
+lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
 pok_security execution
 Processing requirement : one_security_level_by_memory
 -------------------------------------
@@ -14,80 +82,60 @@ Evaluating theorem one_security_level_by_memory
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node1_memory_topsecret
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node1_memory_secret
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node1_memory_unclassified
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node1_memory_driver
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_memory
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_memory_topsecret
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_memory_secret
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_memory_unclassified
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_memory_driver
 Content of set p (lib.real:9:12) is 
 Content of set vp (lib.real:11:13) is 
 Content of set b (lib.real:13:12) is 
-lib.real:15:23 Backends: warning : cardinal of set b is null
-lib.real:15:11 Backends: warning : use default boolean value of true for operator '='
  => Result: TRUE
 
 theorem one_security_level_by_memory is: TRUE
@@ -331,14 +379,6 @@ Content of set p_dest (lib.real:104:17) is
 Content of set vp2 (lib.real:106:14) is 
 Content of set b_dst (lib.real:108:16) is 
 Content of set b_cnx (lib.real:110:16) is 
-lib.real:117:20 Backends: warning : cardinal of set b_dst is null
-lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:119:20 Backends: warning : cardinal of set b_dst is null
-lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
-lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
  => Result: TRUE
 
  * Iterate for variable: main.i_node1_partition_secret
@@ -351,14 +391,6 @@ Content of set p_dest (lib.real:104:17) is
 Content of set vp2 (lib.real:106:14) is 
 Content of set b_dst (lib.real:108:16) is 
 Content of set b_cnx (lib.real:110:16) is 
-lib.real:117:20 Backends: warning : cardinal of set b_dst is null
-lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:119:20 Backends: warning : cardinal of set b_dst is null
-lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
-lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
  => Result: TRUE
 
  * Iterate for variable: main.i_node1_partition_unclassified
@@ -371,14 +403,6 @@ Content of set p_dest (lib.real:104:17) is
 Content of set vp2 (lib.real:106:14) is 
 Content of set b_dst (lib.real:108:16) is 
 Content of set b_cnx (lib.real:110:16) is 
-lib.real:117:20 Backends: warning : cardinal of set b_dst is null
-lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:119:20 Backends: warning : cardinal of set b_dst is null
-lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
-lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_partition_topsecret
@@ -391,14 +415,6 @@ Content of set p_dest (lib.real:104:17) is
 Content of set vp2 (lib.real:106:14) is 
 Content of set b_dst (lib.real:108:16) is 
 Content of set b_cnx (lib.real:110:16) is 
-lib.real:117:20 Backends: warning : cardinal of set b_dst is null
-lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:119:20 Backends: warning : cardinal of set b_dst is null
-lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
-lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_partition_secret
@@ -411,14 +427,6 @@ Content of set p_dest (lib.real:104:17) is
 Content of set vp2 (lib.real:106:14) is 
 Content of set b_dst (lib.real:108:16) is 
 Content of set b_cnx (lib.real:110:16) is 
-lib.real:117:20 Backends: warning : cardinal of set b_dst is null
-lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:119:20 Backends: warning : cardinal of set b_dst is null
-lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
-lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
  => Result: TRUE
 
  * Iterate for variable: main.i_node2_partition_unclassified
@@ -431,14 +439,6 @@ Content of set p_dest (lib.real:104:17) is
 Content of set vp2 (lib.real:106:14) is 
 Content of set b_dst (lib.real:108:16) is 
 Content of set b_cnx (lib.real:110:16) is 
-lib.real:117:20 Backends: warning : cardinal of set b_dst is null
-lib.real:117:15 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:118:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:117:62 Backends: warning : unknown value, use default value of 0.0 for operator Min
-lib.real:119:20 Backends: warning : cardinal of set b_dst is null
-lib.real:119:15 Backends: warning : use default float value of 0.0 for operator Max
-lib.real:120:20 Backends: warning : cardinal of set b_cnx is null
-lib.real:119:62 Backends: warning : use default float value of 0.0 for operator Max
  => Result: TRUE
 
 theorem mils_2 is: TRUE

resources/runtime/python/ocarina/ocarina.py

@@ -73,6 +73,28 @@ def instantiate (root_system):
 
     return runOcarinaFunction (libocarina_python.instantiate, root_system)
 
+################################################################################
+def set_real_theorem (theorem_name):
+    '''Set main REAL theorem
+
+    :param theorem_name: name of the theorem
+    :type theorem_name: string
+
+    '''
+
+    return runOcarinaFunction (libocarina_python.set_real_theorem, theorem_name)
+
+################################################################################
+def add_real_library (libraryname):
+    '''
+
+    :param libraryname: name of the theorem
+    :type libraryname: string
+
+    '''
+
+    return runOcarinaFunction (libocarina_python.add_real_library, libraryname)
+
 ################################################################################
 Backends = Enum ([ "polyorb_hi_ada", "polyorb_hi_c", "real_theorem"])
 '''List of supported backends, used by :data:`generate`'''

resources/runtime/python/test/metrics.py

@@ -9,7 +9,7 @@ def printError(source, messages):
     for message in messages:
         print message
 
-def main(argv):ne
+def main(argv):
     '''Test function'''
     import ocarina;
     import lmp;

resources/runtime/python/test/test.py

 #! /usr/bin/python
 
-import OcarinaPython as ocarina;
-
-def visitor (component,level) :
-    subcomponents=ocarina.AIN.Subcomponents(component);
-    if subcomponents is not None :
-       prefix=''
-       while ( len(prefix)<level ) :
-          prefix=prefix+'.'
-       for child in subcomponents :
-          print prefix,ocarina.getInstanceName(child)[0]
-          visitor(str(ocarina.AIN.Corresponding_Instance(child)),level+1)
+import ocarina
+import lmp
 
 def main ():
     '''Test function'''
 
     err=ocarina.load("rma.aadl");                   # load a file
     print 'load("rma.aadl")'
-    if err[1].strip()!='':
-      print 'info message: \n', err[1]
+    print err
+    if err[1] != None:
+      print 'info message: ', err[1]
     if err[2]!=[]:
-      print 'warning message: \n', err[2]
+      print 'warning message: ', err[2]
     if err[3]!=[]:
-      print 'error message: \n', err[3]
+      print 'error message: ', err[3]
       sys.exit(2)
-      
+
     err=ocarina.load("deployment.aadl");            # load a file
     print 'load("deployment.aadl")'
-    if err[1].strip()!='':
-      print 'info message: \n', err[1]
+    if err[1] != None:
+      print 'info message: ', err[1]
     if err[2]!=[]:
-      print 'warning message: \n', err[2]
+      print 'warning message: ', err[2]
     if err[3]!=[]:
-      print 'error message: \n', err[3]
+      print 'error message: ', err[3]
       sys.exit(2)
-      
+
     err=ocarina.analyze();                          # analyze models
     print 'ocarina.analyze()'
-    if err[1].strip()!='':
-      print 'info message: \n', err[1]
+    if err[1] != None:
+      print 'info message: ', err[1]
     if err[2]!=[]:
-      print 'warning message: \n', err[2]
+      print 'warning message: ', err[2]
     if err[3]!=[]:
-      print 'error message: \n', err[3]
+      print 'error message: ', err[3]
       sys.exit(2)
-      
-    err=ocarina.instantiate("rma.erc32");           # instantiate system
-    print 'ocarina.instantiate("rma.erc32")'
-    if err[1].strip()!='':
-      print 'info message: \n', err[1]
+
+    err=ocarina.instantiate("rma.impl");           # instantiate system
+    print 'ocarina.instantiate("rma.impl")'
+    if err[1] != None:
+      print 'info message: ', err[1]
     if err[2]!=[]:
-      print 'warning message: \n', err[2]
+      print 'warning message: ', err[2]
     if err[3]!=[]:
-      print 'error message: \n', err[3]
+      print 'error message: ', err[3]
       sys.exit(2)
-    
-    print '----------------------------------------------------'
-    print 'Number of Component Instances:'
-    print '----------------------------------------------------'
-    root=ocarina.getInstances('all')[0][0]
-    # root=ocarina.getRoot()
-    print ocarina.getInstanceName(root)[0]
-    visitor(root,1)
 
 if __name__ == "__main__":
     main ()

src/backends/ocarina-backends-real.adb

@@ -32,6 +32,9 @@
 with Ada.Numerics.Generic_Elementary_Functions;
 with Ocarina.Namet;
 with Ocarina.Output;
+with GNAT.OS_Lib; use GNAT.OS_Lib;
+with Ocarina.Options; use Ocarina.Options;
+with Outfiles; use Outfiles;
 
 with Errors; use Errors;
 with Locations; use Locations;
@@ -3199,6 +3202,8 @@ package body Ocarina.Backends.REAL is
       It   : Natural := First;
       Node : Node_Id;
       Success : Boolean;
+      Fd : File_Descriptor;
+
    begin
       Root_System := Instantiate_Model (AADL_Root);
       Exit_On_Error (No (AADL_Root), "Cannot instantiate AADL models");
@@ -3206,6 +3211,10 @@ package body Ocarina.Backends.REAL is
       Success := Analyze (REAL_Language, Root_System);
       Exit_On_Error (not Success, "Cannot analyze REAL specifications");
 
+      if Output_Filename /= No_Name then
+         Fd := Set_Output (Output_Filename);
+      end if;
+
       --  Runtime
 
       while It <= Last (To_Run_Theorem_List) loop
@@ -3243,6 +3252,9 @@ package body Ocarina.Backends.REAL is
 
          It := It + 1;
       end loop;
+
+      Set_Standard_Output;
+      Release_Output (Fd);
    end Generate;
 
    ----------

src/core/model/ocarina-analyzer-real.adb

@@ -148,7 +148,6 @@ package body Ocarina.Analyzer.REAL is
 
    procedure Register_Library_Theorems (REAL_Library : Node_Id) is
       pragma Assert (Kind (REAL_Library) = K_Root_Node);
-      package RNU renames Ocarina.ME_REAL.REAL_Tree.Nutils;
 
       N : Node;
       T : Node_Id;
@@ -210,6 +209,11 @@ package body Ocarina.Analyzer.REAL is
          end loop;
 
       else
+         --  Otherwise, iterate over Library theorems and fetch the
+         --  corresponding theorem.
+
+         RNU.Node_List.Init (To_Run_Theorem_List); --  Reset list of theorems
+
          for J in RNU.Node_List.First .. RNU.Node_List.Last (Library_Theorems)
          loop
             A := Library_Theorems.Table (J).Node;
@@ -292,18 +296,18 @@ package body Ocarina.Analyzer.REAL is
       --  For non-used library theorems, we still analyze them,
       --  since they can be called directly through the API
 
-      --  for J in RNU.Node_List.First ..
-      --    RNU.Node_List.Last (Library_Theorems) loop
-      --     Node := Library_Theorems.Table (J).Node;
+      for J in RNU.Node_List.First ..
+        RNU.Node_List.Last (Library_Theorems) loop
+         Node := Library_Theorems.Table (J).Node;
 
-      --     RNU.REAL_Root := Node;
+         RNU.REAL_Root := Node;
 
-      --     if not Analyze_Sub_Theorem (RNU.REAL_Root) then
-      --        Display_Analyzer_Error
-      --          (Root, "could not proceed to theorem analysis");
-      --        return False;
-      --     end if;
-      --  end loop;
+         if not Analyze_Sub_Theorem (RNU.REAL_Root) then
+            Display_Analyzer_Error
+              (Root, "could not proceed to theorem analysis");
+            return False;
+         end if;
+      end loop;
 
       return True;
    end Analyze_Model;

src/core/tree/ocarina-me_aadl-printers.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---    Copyright (C) 2005-2009 Telecom ParisTech, 2010-2015 ESA & ISAE.      --
+--    Copyright (C) 2005-2009 Telecom ParisTech, 2010-2016 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,11 +29,11 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with GNAT.OS_Lib; use GNAT.OS_Lib;
+with GNAT.OS_Lib;             use GNAT.OS_Lib;
 
-with Ocarina.Namet;           use Ocarina.Namet;
 with Ocarina.Output;          use Ocarina.Output;
-with Ocarina.Options; use Ocarina.Options;
+with Ocarina.Options;         use Ocarina.Options;
+with Outfiles;                use Outfiles;
 
 package body Ocarina.ME_AADL.Printers is
 
@@ -42,13 +42,14 @@ package body Ocarina.ME_AADL.Printers is
    ---------------------
 
    procedure Print_AADL_Tree (Node : Node_Id; W : W_Node_Spg) is
+      Fd : File_Descriptor;
    begin
       if Output_Filename /= No_Name then
-         Get_Name_String (Output_Filename);
-         Set_Output (Create_File (Name_Buffer (1 .. Name_Len), Binary));
+         Fd := Set_Output (Output_Filename);
       end if;
       W.all (Node);
       Set_Standard_Output;
+      Release_Output (Fd);
    end Print_AADL_Tree;
 
 end Ocarina.ME_AADL.Printers;

src/frontends/real/ocarina-fe_real-parser.adb

@@ -1916,6 +1916,32 @@ package body Ocarina.FE_REAL.Parser is
       end if;
    end Process;
 
+   -----------------------
+   -- Load_REAL_Library --
+   -----------------------
+
+   procedure Load_REAL_Library (File_Name : Name_Id) is
+      use Ocarina.Files;
+      use Ocarina.Namet;
+
+      Buffer            : Location;
+      REAL_External_Lib : Node_Id;
+   begin
+      Buffer := Load_File (File_Name);
+      if Buffer = No_Location then
+         Display_And_Exit
+           ("could not load file " &
+              Get_Name_String (File_Name));
+      end if;
+
+      REAL_External_Lib := Process (No_Node, Buffer);
+      if No (REAL_External_Lib) then
+         Display_And_Exit ("could not parse REAL specification");
+      end if;
+
+      Register_Library_Theorems (REAL_External_Lib);
+   end Load_REAL_Library;
+
    ----------
    -- Init --
    ----------
@@ -1934,26 +1960,7 @@ package body Ocarina.FE_REAL.Parser is
       --  parse and register it.
 
       for J in REAL_Libs.First .. REAL_Libs.Last loop
-         declare
-            use Ocarina.Files;
-
-            Buffer            : Location;
-            REAL_External_Lib : Node_Id;
-         begin
-            Buffer := Load_File (REAL_Libs.Table (J));
-            if Buffer = No_Location then
-               Display_And_Exit
-                 ("could not load file " &
-                  Get_Name_String (REAL_Libs.Table (J)));
-            end if;
-
-            REAL_External_Lib := Process (No_Node, Buffer);
-            if No (REAL_External_Lib) then
-               Display_And_Exit ("could not parse REAL specification");
-            end if;
-
-            Register_Library_Theorems (REAL_External_Lib);
-         end;
+         Load_REAL_Library (REAL_Libs.Table (J));
       end loop;
    end Init;
 

src/frontends/real/ocarina-fe_real-parser.ads

@@ -48,6 +48,8 @@ package Ocarina.FE_REAL.Parser is
    procedure Init;
    --  Initialize the parser
 
+   procedure Load_REAL_Library (File_Name : Name_Id);
+
    package REAL_Libs is new GNAT.Table (Name_Id, Nat, 1, 10, 10);
    --  Table of REAL libraries to consider
 

src/main/ocarina-cmd_line.adb

@@ -192,7 +192,7 @@ package body Ocarina.Cmd_Line is
    begin
       Set_Usage (Ocarina_Options, Usage => "[switches] <aadl_files>");
 
-      --  Note: the order of call to Define_Switch dictate the order
+      --  Note: the order of call to Define_Switch dictates the order
       --  of information when calling GNAT.Command_Line.Display_Help.
 
       --  --help flag, just so that it appears in the online help
@@ -294,7 +294,7 @@ package body Ocarina.Cmd_Line is
 
       --  -real_theorem flag
       Define_Switch (Ocarina_Options, "-real_theorem:",
-                     Help => "Name of the main theorem to evaluate");
+                     Help => "Name of the main REAL theorem to evaluate");
 
       --  -real_lib flag
       Define_Switch (Ocarina_Options, "-real_lib:",

src/python/ocarina-python_cmd.adb

@@ -193,6 +193,44 @@ package body Ocarina.Python_Cmd is
       Set_Return_Value (Data, Result);
    end On_Instantiate;
 
+   -------------------------
+   -- On_Set_REAL_Theorem --
+   -------------------------
+
+   procedure On_Set_REAL_Theorem
+     (Data : in out Callback_Data'Class; Command : String);
+
+   procedure On_Set_REAL_Theorem
+     (Data : in out Callback_Data'Class;
+      Command : String)
+   is
+      pragma Unreferenced (Command);
+      Result : constant Boolean :=
+        Ocarina.Utils.Set_REAL_Theorem (Nth_Arg (Data, 1, ""));
+
+   begin
+      Set_Return_Value (Data, Result);
+   end On_Set_REAL_Theorem;
+
+   -------------------------
+   -- On_Add_REAL_Library --
+   -------------------------