Commit 365dd7ca authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Adapt to the new Rdbg Plugin interface.

cf rdbg git 66d01f567940e06eab9a49604663d43c29fdfe01
parent 53d82954
......@@ -151,11 +151,19 @@ let (step : Data.subst list -> Data.subst list)=
);
bounds
let _ =
OcamlRM.reg_inputs "rabbit.cmxs" inputs;
OcamlRM.reg_outputs "rabbit.cmxs" outputs;
OcamlRM.reg_kill "rabbit.cmxs" kill;
OcamlRM.reg_step "rabbit.cmxs" step;
OcamlRM.reg_mems "rabbit.cmxs" mems_i mems_o
open RdbgPlugin
let plugin = {
inputs = inputs;
outputs= outputs;
kill= kill;
init_inputs=mems_i;
init_outputs=mems_o;
step= step;
step_dbg=(fun _ _ -> assert false);
}
let _ =
OcamlRM.reg_plugin "rabbit.cmxs" plugin;
......@@ -7,11 +7,14 @@ let oc = open_out "call_foo.rif"
(* node main(a:int; b:bool; c:real) returns ( x:int; y:bool; z:real) = *)
open Data
open RdbgPlugin
let _ =
let inputs, outputs, kill, step, step_dbg, mems_i,mems_o =
let args = Array.of_list ["../../../bin/lutin";"foo.lut";"-n";"main";"-seed";"1"] in
LutinRun.make_lut args
let plugin = LutinRun.make args in
plugin.inputs,plugin.outputs,plugin.kill,plugin.step,plugin.step_dbg,
plugin.init_inputs,plugin.init_outputs
in
......
(* Time-stamp: <modified the 20/02/2014 (at 10:25) by Erwan Jahier> *)
(* Time-stamp: <modified the 27/03/2014 (at 09:41) by Erwan Jahier> *)
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
*)
......@@ -8,6 +8,7 @@ type vars = (string * Data.t) list
open Lv6MainArgs
open Soc
open SocExecValue
open RdbgPlugin
let make argv =
let opt = Lv6MainArgs.parse argv in
......@@ -85,5 +86,13 @@ let make argv =
in
let (mems_in : Data.subst list) = [] in (* XXX todo *)
let (mems_out : Data.subst list) = [] in (* XXX todo *)
vntl_i,vntl_o, (fun _ -> ()), step, step_dbg, mems_in, mems_out
{
inputs = vntl_i;
outputs= vntl_o;
kill=(fun _ -> ());
init_inputs=mems_in;
init_outputs=mems_out;
step=step;
step_dbg=step_dbg;
}
(* Time-stamp: <modified the 26/03/2014 (at 17:56) by Erwan Jahier> *)
type vars = (string * Data.t) list
val make: string array ->
vars * vars * (string -> unit)
* (Data.subst list -> Data.subst list)
* (Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
val make: string array -> RdbgPlugin.t
......@@ -65,7 +65,7 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
)
)
open RdbgPlugin
let (make_rp_list : reactive_program list ->
vars list * vars list * (string -> unit) list *
(Data.subst list -> Data.subst list) list *
......@@ -74,17 +74,21 @@ let (make_rp_list : reactive_program list ->
fun rpl ->
let add_init init (a,b,c,d,e) = (a,b,c,d,e,init,init) in
let aux rp =
let ins, outs, kill, step, step_dbg, initin, initout =
let plugin =
match rp with
(* | LustreV6(prog,node) -> add_init [] (LustreRun.make_v6 prog node) *)
| LustreV6(args) -> Lus2licRun.make args
| LustreV4(prog,node) -> add_init [] (LustreRun.make_v4 prog node)
| LustreEc(prog) -> add_init [] (LustreRun.make_ec prog)
| LustreEcExe(prog) -> add_init [] (LustreRun.make_ec_exe prog)
| Socket(addr, port) -> add_init [] (LustreRun.make_socket addr port)
| LustreV4(prog,node) -> LustreRun.make_v4 prog node
| LustreEc(prog) -> LustreRun.make_ec prog
| LustreEcExe(prog) -> LustreRun.make_ec_exe prog
| Socket(addr, port) -> LustreRun.make_socket addr port
| SocketInit(addr, port) -> LustreRun.make_socket_init addr port
| Ocaml(cmxs) -> OcamlRun.make_ocaml cmxs
| Lutin(args) -> LutinRun.make_lut args
| Lutin(args) -> LutinRun.make args
in
let ins, outs, kill, step, step_dbg, initin, initout =
plugin.inputs,plugin.outputs,plugin.kill,plugin.step,plugin.step_dbg,
plugin.init_inputs,plugin.init_outputs
in
let step = if args.debug_ltop then
let (string_of_subst : Data.subst -> string) =
......
(* Time-stamp: <modified the 21/02/2014 (at 16:02) by Erwan Jahier> *)
(* Time-stamp: <modified the 26/03/2014 (at 17:07) by Erwan Jahier> *)
(* generate ocaml glue code that makes it possible to call lutin
from ocaml with the current set of arguments.
......@@ -24,9 +24,9 @@ let (f: string array -> MainArg.t -> unit) =
let oc = open_out (outfile) in
let entete = Util.entete "(*" "*)" in
Printf.fprintf oc "%s
let inputs, outputs, kill, step, step_dbg, mems_i,mems_o =
let plugin =
let args = Array.of_list [%s] in
LutinRun.make_lut args
LutinRun.make args
(* The following is to make it possible for rdbg to call this lutin program.
But of course, one can use it to dynamically call those steps functions from
......@@ -34,10 +34,5 @@ any ocaml programs (as rdbg does).
*)
let dyn_file = (Dynlink.adapt_filename \"%s\")
let _ =
OcamlRM.reg_inputs dyn_file inputs;
OcamlRM.reg_outputs dyn_file outputs;
OcamlRM.reg_kill dyn_file kill;
OcamlRM.reg_step dyn_file step;
OcamlRM.reg_step_dbg dyn_file step_dbg;
OcamlRM.reg_mems dyn_file mems_i mems_o
OcamlRM.reg_plugin dyn_file plugin
" entete args_str cma_file
......@@ -654,7 +654,7 @@ old: lucky luc2luciole luc4c liblucky_nc.a libluc4c_nc.a
compile_all: gen_version $(OBJDIR) gnuplot-rif gnuplot-socket call-via-socket draw-all $(LUCKY_DEF) lutin check-rif ltop lut4ocaml-clean lut4ocaml-all
rest: lut4ocaml-clean lut4ocaml-all
rest: check-rif ltop lut4ocaml-clean lut4ocaml-all
allnc: clean lucky ltop show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2luciole luc4c libluc4c_nc.a draw-all lut4ocaml-all check-rif
static: lucky_static ltop_static show_static stubs_static gen_luc_static
......@@ -784,3 +784,8 @@ lutin-labo-install:
labo: lutin-labo-install
rdbg:
cp -rf $(CAML_INSTALL_DIR)/lutin/ ~/rdbg/www/plugins/$(HOSTTYPE)-ocaml$(shell $(OCAMLC) -version)/
cp -rf $(CAML_INSTALL_DIR)/lustre-v6/ ~/rdbg/www/plugins/$(HOSTTYPE)-ocaml$(shell $(OCAMLC) -version)/
cp ~/lus2lic/linux/bin/lus2lic ~/rdbg/www/plugins/$(HOSTTYPE)-ocaml$(shell $(OCAMLC) -version)/bin/
cp $(OBJDIR)/lutin ~/rdbg/www/plugins/$(HOSTTYPE)-ocaml$(shell $(OCAMLC) -version)/bin/
(* Time-stamp: <modified the 26/03/2014 (at 17:46) by Erwan Jahier> *)
open RdbgPlugin
type vars = (string * Data.t) list
let debug = ref false
......@@ -49,15 +51,13 @@ let get_io_from_lustre a b =
(* XXX Doable with DynLink? Or via Ezdl? *)
let (make_ec : string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
let (make_ec : string -> RdbgPlugin.t) =
fun ec_file ->
let ec_in, ec_out = get_io_from_lustre ec_file None in
let (ec_stdin_in, ec_stdin_out) = Unix.pipe () in
let (ec_stdout_in, ec_stdout_out) = Unix.pipe () in
let ec_ic = Unix.in_channel_of_descr ec_stdout_in in
let ec_oc = Unix.out_channel_of_descr ec_stdin_out in
......@@ -69,18 +69,18 @@ let (make_ec : string -> vars * vars * (string -> unit) *
let arg_list = ["ecexe"^(Util.exe ()); "-r"; "-rif"; ec_file] in
let arg_array = Array.of_list arg_list in
let prog = List.hd arg_list in
try
if !debug then (
List.iter (fun x -> output_string stderr (x ^ " ")) arg_list;
output_string stderr "\n";
flush stderr
);
Unix.create_process prog arg_array
ec_stdin_in ec_stdout_out ec_stdout_out
with Unix.Unix_error(e,_, prog) ->
let msg = Unix.error_message e in
Printf.eprintf "*** Error when creating process with %s: %s\n" prog msg;
exit 2
try
if !debug then (
List.iter (fun x -> output_string stderr (x ^ " ")) arg_list;
output_string stderr "\n";
flush stderr
);
Unix.create_process prog arg_array
ec_stdin_in ec_stdout_out ec_stdout_out
with Unix.Unix_error(e,_, prog) ->
let msg = Unix.error_message e in
Printf.eprintf "*** Error when creating process with %s: %s\n" prog msg;
exit 2
in
let _ = Printf.eprintf "Process %d (ecexe) created\n" pid_lustre; flush stderr in
let kill msg =
......@@ -112,12 +112,18 @@ let (make_ec : string -> vars * vars * (string -> unit) *
Event.terminate = ctx.Event.ctx_terminate;
}
in
ec_in, ec_out, kill, step, step_dbg
{
inputs = ec_in;
outputs= ec_out;
kill= kill;
init_inputs= [];
init_outputs= [];
step = step;
step_dbg = step_dbg
}
(* Via une edition de liens dynamique *)
let (make_ec_dynlink: string -> string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list)) =
let (make_ec_dynlink: string -> string -> string -> RdbgPlugin.t) =
fun node ec_file dl_file ->
let ec_in, ec_out = get_io_from_lustre ec_file None in
let dl = Ezdl.dlopen dl_file in
......@@ -131,9 +137,7 @@ let (make_ec_dynlink: string -> string -> string -> vars * vars * (string -> uni
assert false
(**********************************************************************************)
let (make_v6 : string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
let (make_v6 : string -> string -> RdbgPlugin.t) =
fun lus_file node ->
let dir = Filename.dirname lus_file in
if Util2.lv62ec lus_file node dir then
......@@ -142,9 +146,7 @@ let (make_v6 : string -> string -> vars * vars * (string -> unit) *
failwith ("Error when compiling " ^ lus_file ^ " with node " ^ node ^"\n")
(**********************************************************************************)
let (make_v4 : string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
let (make_v4 : string -> string -> RdbgPlugin.t) =
fun lus_file node ->
let dir = Filename.dirname lus_file in
if Util2.lv42ec lus_file node dir then
......@@ -170,9 +172,7 @@ let rec connect_loop sock addr k =
else failwith "lustreRun: cannot connect to the socket"
let (make_socket_do : string -> int -> in_channel *
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
let (make_socket_do : string -> int -> in_channel * RdbgPlugin.t) =
fun sock_adr port ->
let _ =
if !debug then (
......@@ -191,7 +191,7 @@ let (make_socket_do : string -> int -> in_channel *
with
Unix.Unix_error(errcode, funcstr, paramstr) ->
failwith ("LustreRun connect failure: " ^ (Unix.error_message errcode) ^
"(" ^ funcstr ^ " " ^ paramstr ^")\n")
"(" ^ funcstr ^ " " ^ paramstr ^")\n")
in
let kill msg =
Printf.printf "Killing the socket process (%s:%i)\n" sock_adr port;
......@@ -200,10 +200,10 @@ let (make_socket_do : string -> int -> in_channel *
output_string sock_out msg;
flush sock_out;
let str = input_line sock_in in
(* make sure that the sut process has read the quit before closing socks *)
print_string (str ^"\n");
flush stdout;
Unix.shutdown sock Unix.SHUTDOWN_ALL
(* make sure that the sut process has read the quit before closing socks *)
print_string (str ^"\n");
flush stdout;
Unix.shutdown sock Unix.SHUTDOWN_ALL
in
let label = Printf.sprintf "[%s:%i] " sock_adr port in
let vars_in, vars_out =
......@@ -229,37 +229,40 @@ let (make_socket_do : string -> int -> in_channel *
Event.terminate = ctx.Event.ctx_terminate;
}
in
if !debug then (
Printf.fprintf stderr "\nInterface declarations on %s:%i, ok.\n" sock_adr port;
flush stderr
);
sock_in, vars_in, vars_out, kill, step, step_dbg
let plugin = {
inputs = vars_in;
outputs= vars_out;
kill= kill;
init_inputs= [];
init_outputs= [];
step = step;
step_dbg = step_dbg
}
in
if !debug then (
Printf.fprintf stderr "\nInterface declarations on %s:%i, ok.\n" sock_adr port;
flush stderr
);
sock_in, plugin
(* exported *)
let (make_socket : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)) =
let (make_socket : string -> int -> RdbgPlugin.t) =
fun sock_adr port ->
let _, vars_in, vars_out, kill, step,step_dbg = make_socket_do sock_adr port in
vars_in, vars_out, kill, step, step_dbg
let _, p = make_socket_do sock_adr port in
p
(* exported *)
let (make_socket_init : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) *
Data.subst list * Data.subst list) =
let (make_socket_init : string -> int -> RdbgPlugin.t) =
fun sock_adr port ->
let sock_in, vars_in, vars_out, kill, step, step_dbg = make_socket_do sock_adr port in
let out_init = RifIO.read sock_in None vars_out in
let in_init = RifIO.read sock_in None vars_in in
vars_in, vars_out, kill, step, step_dbg, in_init, out_init
let sock_in, p = make_socket_do sock_adr port in
let out_init = RifIO.read sock_in None p.outputs in
let in_init = RifIO.read sock_in None p.inputs in
{ p with
init_inputs= in_init;
init_outputs= out_init;
}
(**********************************************************************************)
let (make_ec_exe : string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
) =
let (make_ec_exe : string -> RdbgPlugin.t) =
fun ec_file ->
let exe = (Filename.chop_extension ec_file) ^ (Util.exe()) in
let _ = if not (Sys.file_exists exe) then (
......@@ -328,7 +331,15 @@ let (make_ec_exe : string -> vars * vars * (string -> unit) *
Event.terminate = ctx.Event.ctx_terminate;
}
in
ec_in, ec_out, kill, step, step_dbg
{
inputs = ec_in;
outputs= ec_out;
kill= kill;
init_inputs= [];
init_outputs= [];
step = step;
step_dbg = step_dbg
}
(**********************************************************************************)
......
......@@ -11,8 +11,6 @@
Should I use functors instead ???
*)
(* var name and var type list *)
type vars = (string * Data.t) list
(** [make_ec ec_file.ec] handles ec programs (expanded code coming from
......@@ -20,27 +18,19 @@ type vars = (string * Data.t) list
Raises Failure of string if something bas happens.
*)
val make_ec : string ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
val make_ec : string -> RdbgPlugin.t
(* [make_ec_exe ec_file.ec] supposes that ec_file.ec has already been compiled
into an executable that is named ec_file.
*)
val make_ec_exe : string ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
val make_ec_exe : string -> RdbgPlugin.t
(** [make_v6 file node] handles Verimag/Lustre v6 programs
Raises Failure of string if something bas happens.
*)
val make_v6 : string -> string ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
val make_v6 : string -> string -> RdbgPlugin.t
val make_v4 : string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
val make_v4 : string -> string -> RdbgPlugin.t
(** [make_socket sock_addr port]
......@@ -52,15 +42,12 @@ val make_v4 : string -> string -> vars * vars * (string -> unit) *
The process that feeds the other side of the socket is supposed
to stop if it receives "#quit".
*)
val make_socket : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
val make_socket : string -> int -> RdbgPlugin.t
val make_socket_init : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
val make_socket_init : string -> int -> RdbgPlugin.t
(* var name and var type list *)
type vars = (string * Data.t) list
(** [make_luciole dro_file inputs outputs]
fails if dro_file does not exists, or if its interface is not
......
(* Time-stamp: <modified the 24/02/2014 (at 10:41) by Erwan Jahier> *)
(* Time-stamp: <modified the 26/03/2014 (at 17:06) by Erwan Jahier> *)
(**********************************************************************************)
type vars = (string * Data.t) list
......@@ -19,7 +19,9 @@ let (to_vals : Data.subst list -> Value.OfIdent.t) =
(fun acc (n,v) -> Value.OfIdent.add acc (n, Value.from_data_val v))
Value.OfIdent.empty
let make_lut argv =
open RdbgPlugin
let make argv =
let opt = MainArg.parse argv in
let prog = MainArg.infile opt
and node = MainArg.main_node opt
......@@ -28,10 +30,10 @@ let make_lut argv =
let lut_in = List.map var_to_var_pair (LutExe.in_var_list lut_mach) in
let lut_out = List.map var_to_var_pair (LutExe.out_var_list lut_mach) in
let lut_memories =
(* if LtopArg.args.LtopArg.delay_env_outputs then *)
(* LutExe.get_init_pres lut_mach *)
(* else *)
Value.OfIdent.empty
(* if LtopArg.args.LtopArg.delay_env_outputs then *)
(* LutExe.get_init_pres lut_mach *)
(* else *)
Value.OfIdent.empty
in
let ctrl_state = ref (LutExe.get_init_state lut_mach) in
let data_state = ref
......@@ -43,9 +45,9 @@ let make_lut argv =
let lut_step sl =
let _ = data_state := { !data_state with LutExe.ins = to_vals sl } in
let new_cs, new_ds = LutExe.step lut_mach !ctrl_state !data_state in
ctrl_state := new_cs;
data_state := new_ds;
to_subst_list lut_out new_ds.LutExe.outs
ctrl_state := new_cs;
data_state := new_ds;
to_subst_list lut_out new_ds.LutExe.outs
in
let (lut_step_dbg:
Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) =
......@@ -56,28 +58,28 @@ let make_lut argv =
data_state := new_ds;
cont (to_subst_list lut_out new_ds.LutExe.outs) ctx
in
data_state := { !data_state with LutExe.ins = to_vals sl };
(* { (* XXX l'enlever quand j'aurais trouvé le bon endroit dans lutExe ?? *) *)
(* Event.step = ctx.Event.ctx_step; *)
(* Event.kind = "lutin_step prog='" ^ (String.concat "," prog) ^ *)
(* "' node ='" ^ node ^ "' \n dump expr =" ^ *)
(* (LutExe.string_of_control_state !ctrl_state) ^ " \n stack : " *)
(* (* ^ *) *)
(* (* (CoIdent.string_of_src_stack ()) *) *)
(* ; *)
(* Event.data = ctx.Event.ctx_data; *)
(* Event.next = (fun () -> *)
LutExe.step_ldbg ctx node lut_mach !ctrl_state !data_state cont_lut_step
(* Event.terminate = ctx.Event.ctx_terminate; *)
(* } *)
data_state := { !data_state with LutExe.ins = to_vals sl };
(* { (* XXX l'enlever quand j'aurais trouvé le bon endroit dans lutExe ?? *) *)
(* Event.step = ctx.Event.ctx_step; *)
(* Event.kind = "lutin_step prog='" ^ (String.concat "," prog) ^ *)
(* "' node ='" ^ node ^ "' \n dump expr =" ^ *)
(* (LutExe.string_of_control_state !ctrl_state) ^ " \n stack : " *)
(* (* ^ *) *)
(* (* (CoIdent.string_of_src_stack ()) *) *)
(* ; *)
(* Event.data = ctx.Event.ctx_data; *)
(* Event.next = (fun () -> *)
LutExe.step_ldbg ctx node lut_mach !ctrl_state !data_state cont_lut_step
(* Event.terminate = ctx.Event.ctx_terminate; *)
(* } *)
in
let mems_in =
List.fold_left
(fun acc (vn,_vt) ->
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
)
[]
lut_in
......@@ -85,15 +87,23 @@ let make_lut argv =
let mems_out =
List.fold_left
(fun acc (vn,_vt) ->
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
)
[]
lut_out
in
lut_in, lut_out, (fun _ -> ()), lut_step, lut_step_dbg, mems_in, mems_out
{
inputs = lut_in;
outputs= lut_out;
kill=(fun _ -> ());
init_inputs=mems_in;
init_outputs=mems_out;
step=lut_step;
step_dbg=lut_step_dbg;
}
......
(* Time-stamp: <modified the 24/02/2014 (at 10:40) by Erwan Jahier> *)
(* Time-stamp: <modified the 26/03/2014 (at 17:03) by Erwan Jahier> *)
type vars = (string * Data.t) list
val make_lut: string array ->
vars * vars * (string -> unit)
* (Data.subst list -> Data.subst list)
* (Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
val make: string array -> RdbgPlugin.t
......@@ -103,9 +103,10 @@ let rif_all = rif_in @ rif_out
(**************************************************************************)
(* Oracle launching *)
open RdbgPlugin
let oracle_in, oracle_out, kill_oracle, step_oracle, step_oracle_dbg =
LustreRun.make_ec arg.ec
let plugin = LustreRun.make_ec arg.ec in
plugin.inputs,plugin.outputs,plugin.kill,plugin.step,plugin.step_dbg
(**************************************************************************)
(* Check that the set of oracle Inputs is included in the set of the
......
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