Commit 73f0aedf authored by yoogx's avatar yoogx
Browse files

* Take into account the Output_Filename variable to store REAL

          output in a separate file
parent 1f8c026c
......@@ -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;
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;
Release_Output (Fd);
end Generate;
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