diff --git a/src/_tags.in b/src/_tags.in
index 52f1f08c0eb569456a85444fdddbfee5154f0e27..786f036db2e4be1a2e899cd2b05568d572600a2e 100644
--- a/src/_tags.in
+++ b/src/_tags.in
@@ -7,6 +7,7 @@ true: bin_annot, color(always)
"checks": include
"parsers": include
"backends": include
+"backends/Ada": include
"backends/C": include
"backends/Horn": include
"backends/EMF": include
diff --git a/src/backends/Ada/.merlin b/src/backends/Ada/.merlin
new file mode 100644
index 0000000000000000000000000000000000000000..2fb3f0bc1e7fdfef783204d7f14fd522a606bd77
--- /dev/null
+++ b/src/backends/Ada/.merlin
@@ -0,0 +1 @@
+REC
\ No newline at end of file
diff --git a/src/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a5f555dd12e34c2bb3cc8214d0f758d093f16a0e
--- /dev/null
+++ b/src/backends/Ada/ada_backend.ml
@@ -0,0 +1,22 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - ISAE-SUPAERO *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Format
+
+let translate_to_ada basename prog machines dependencies =
+ let module Ads = Ada_backend_ads.Main in
+ let module Adb = Ada_backend_adb.Main in
+ let module Wrapper = Ada_backend_wrapper.Main in
+ print_endline "Ada code generated!"
+
+(* Local Variables: *)
+(* compile-command:"make -C ../../.." *)
+(* End: *)
diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
new file mode 100644
index 0000000000000000000000000000000000000000..57515bb0dfec21f306dd425b6f62f57cda195789
--- /dev/null
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -0,0 +1,14 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - ISAE-SUPAERO *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+module Main =
+struct
+end
diff --git a/src/backends/Ada/ada_backend_ads.ml b/src/backends/Ada/ada_backend_ads.ml
new file mode 100644
index 0000000000000000000000000000000000000000..57515bb0dfec21f306dd425b6f62f57cda195789
--- /dev/null
+++ b/src/backends/Ada/ada_backend_ads.ml
@@ -0,0 +1,14 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - ISAE-SUPAERO *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+module Main =
+struct
+end
diff --git a/src/backends/Ada/ada_backend_wrapper.ml b/src/backends/Ada/ada_backend_wrapper.ml
new file mode 100644
index 0000000000000000000000000000000000000000..57515bb0dfec21f306dd425b6f62f57cda195789
--- /dev/null
+++ b/src/backends/Ada/ada_backend_wrapper.ml
@@ -0,0 +1,14 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - ISAE-SUPAERO *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+module Main =
+struct
+end
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index 9d06ac0616287e22d3cfdca2765871245b6462aa..e07d8342fa29373f7649bbe62f91e52677a425d8 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -9,7 +9,7 @@ let dynamic_checks () =
match !Options.output, !Options.spec with
| "C", "C" -> true
| _ -> false
-
+
(* check whether a source file has a compiled header, if not, generate the
compiled header *)
@@ -68,7 +68,7 @@ let stage1 prog dirname basename =
let orig, prog =
if !Options.global_inline && !Options.main_node <> "" then
(if !Options.witnesses then prog else []),
- Inliner.global_inline basename prog
+ Inliner.global_inline basename prog
else (* if !Option.has_local_inline *)
[],
Inliner.local_inline prog (* type_env clock_env *)
@@ -88,7 +88,7 @@ let stage1 prog dirname basename =
(* Registering and checking machine types *)
if Machine_types.is_active then Machine_types.load prog;
-
+
(* Generating a .lusi header file only *)
if !Options.lusi then
@@ -96,12 +96,12 @@ let stage1 prog dirname basename =
exported as a lusi *)
raise (StopPhase1 prog);
- (* Optimization of prog:
- - Unfold consts
+ (* Optimization of prog:
+ - Unfold consts
- eliminate trivial expressions
*)
(*
- let prog =
+ let prog =
if !Options.const_unfold || !Options.optimization >= 5 then
begin
Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
@@ -139,7 +139,7 @@ let stage1 prog dirname basename =
Clock_calculus.uneval_prog_generics prog;
-(* Disabling witness option. Could but reactivated later
+(* Disabling witness option. Could but reactivated later
if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
begin
let orig = Corelang.copy_prog orig in
@@ -154,7 +154,7 @@ let stage1 prog dirname basename =
!Options.main_node
orig prog type_env clock_env
end;
-*)
+*)
(* Computes and stores generic calls for each node,
only useful for ANSI C90 compliant generic node compilation *)
@@ -201,19 +201,19 @@ let stage1 prog dirname basename =
Access.check_prog prog;
end;
-
+
let prog = SortProg.sort_nodes_locals prog in
-
+
prog, dependencies
(* from source to machine code, with optimization *)
-let stage2 prog =
+let stage2 prog =
(* Computation of node equation scheduling. It also breaks dependency cycles
and warns about unused input or memory variables *)
Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
let prog, node_schs =
- try
+ try
Scheduling.schedule_prog prog
with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
systemtic way in AlgebraicLoop module *)
@@ -226,7 +226,7 @@ let stage2 prog =
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
- (* TODO Salsa optimize prog:
+ (* TODO Salsa optimize prog:
- emits warning for programs with pre inside expressions
- make sure each node arguments and memory is bounded by a local annotation
- introduce fresh local variables for each real pure subexpression
@@ -238,14 +238,14 @@ let stage2 prog =
Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ " Machine_code_common.pp_machines machine_code);
(* Optimize machine code *)
- Optimize_machine.optimize prog node_schs machine_code
+ Optimize_machine.optimize prog node_schs machine_code
(* printing code *)
let stage3 prog machine_code dependencies basename =
let basename = Filename.basename basename in
match !Options.output with
- "C" ->
+ "C" ->
begin
Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
C_backend.translate_to_c
@@ -262,6 +262,12 @@ let stage3 prog machine_code dependencies basename =
Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
end
+ | "Ada" ->
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@,");
+ Ada_backend.translate_to_ada
+ basename prog machine_code dependencies
+ end
| "horn" ->
begin
let destname = !Options.dest_dir ^ "/" ^ basename in
diff --git a/src/options_management.ml b/src/options_management.ml
index 19dc05262ce8f8cfe3f40e249679d05e87bf376b..3014d5ed8bf75c5c5975a00780d03501fa35ca86 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Options
-
+
let print_version () =
Format.printf "Lustrec compiler, version %s (%s)@." version codename;
Format.printf "Standard lib: %s@." Version.include_path;
@@ -21,13 +21,13 @@ let add_include_dir dir =
let removed_slash_suffix =
let len = String.length dir in
if dir.[len-1] = '/' then
- String.sub dir 0 (len - 1)
+ String.sub dir 0 (len - 1)
else
dir
in
include_dirs := removed_slash_suffix :: !include_dirs
-
+
(** Solving the path of required library:
If local: look in the folders described in !Options.include_dirs
If non local: look first as a local, then in Version.include_path:
@@ -41,7 +41,7 @@ let search_lib_path (local, full_file_name) =
List.fold_right (fun dir res ->
match res with Some _ -> res
| None ->
- let path_to_lib = dir ^ "/" ^ full_file_name in
+ let path_to_lib = dir ^ "/" ^ full_file_name in
if Sys.file_exists path_to_lib then
Some dir
else
@@ -57,11 +57,11 @@ let search_lib_path (local, full_file_name) =
(* Search for path of core libs (without lusic: arrow and io_frontend *)
let core_dependency lib_name =
search_lib_path (false, lib_name ^ ".h")
-
+
let name_dependency (local, dep) =
let dir = search_lib_path (false, dep ^ ".lusic") in
dir ^ "/" ^ dep
-
+
let set_mpfr prec =
if prec > 0 then (
mpfr := true;
@@ -79,7 +79,7 @@ let set_real_type s =
real_type := "mpfr";
)
| _ -> real_type := s
-
+
let set_backend s =
output := s;
Backends.setup ()
@@ -90,15 +90,15 @@ let common_options =
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
"-print-types", Arg.Set print_types, "prints node types";
"-print-clocks", Arg.Set print_clocks, "prints node clocks";
- "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
- "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>";
+ "-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops";
+ "-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>";
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
"-version", Arg.Unit print_version, " displays the version";
]
let lustrec_options =
common_options @
- [
+ [
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
"-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
@@ -108,6 +108,7 @@ let lustrec_options =
"-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
"-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
(* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
+ "-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C";
"-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
"-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
"-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
@@ -119,7 +120,7 @@ let lustrec_options =
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
"-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
-
+
"-c++" , Arg.Set cpp , "c++ backend";
"-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";
"-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)";
@@ -140,7 +141,7 @@ let lustret_options =
let plugin_opt (name, activate, options) =
( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
-
+
let get_witness_dir filename =
(* Make sure the directory exists *)