Commit 460b996f authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Use lurettetop to talk to Alices (instead of Lutin) plus various improvements.

Still no reg test.
parent 9b3e5fc8
......@@ -270,8 +270,6 @@ LURETTE_SOURCES=\
$(OBJDIR)/rif.ml \
$(OBJDIR)/coverage.mli \
$(OBJDIR)/coverage.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
LUTIN_SOURCES = \
$(OBJDIR)/version.ml \
......
......@@ -149,7 +149,7 @@ structTab "^alice_name^"::memories;
}
catch (ImsMessageStack& xMessageStack)
{
xMessageStack.InsertErrorMessage(\""^alice_name^"\", \"Err\", cImsFatal, IMS_DEBUG_INFO("^
xMessageStack.InsertErrorMessage(\"2\", \"Err\", cImsFatal, IMS_DEBUG_INFO("^
alice_name^":Initialisation))
<< \" Erreur lors de l'initialisation du contexte de "^fn^"\";
throw xMessageStack;
......@@ -263,10 +263,7 @@ let (gen_alice_stub_h : alice_args -> unit) =
#endif // BUILD_"^amn^"
extern \"C\"
{
#include \""^fn^".h\"
}
#include \""^fn^".h\"
class "^amn^"_interface "^amn^";
......
......@@ -15,7 +15,7 @@
open LucProg
type gen_mode = Lustre | Scade | Alice | Luciole | Nop
type gen_mode = Lustre | Scade | Alices | Luciole | Nop
type step_mode = Inside | Edges | Vertices
let step_mode_to_str = function
......@@ -200,11 +200,11 @@ let (gen_h_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit
let put s = output_string oc s in
let putln s = output_string oc (s^"\n") in
let max_buff_size =
(* 10 digits per I/O is enough? *)
let in_nb = List.length in_vars in
let out_nb = List.length out_vars in
let io_size = 10 in
2 lsl (int_of_float (log (float_of_int (20+io_size*(in_nb+out_nb))) /. (log 2.)))
(* 10 digits per I/O is enough? *)
let io_size = 100 in
max 2048 (2 lsl (int_of_float (log (float_of_int (20+io_size*(in_nb+out_nb))) /. (log 2.))))
in
let put_var_decl_in_struct var =
put " ";
......@@ -239,7 +239,6 @@ typedef float _float;
";
if option.use_sockets then (
putln ("#define MAX_BUFF_SIZE "^(string_of_int max_buff_size)^"");
putln ("#define MAX_BUFF_SIZE_4 "^(string_of_int (4*max_buff_size))^"");
);
putln "//--------- Pragmas ----------------";
putln ("//MODULE: " ^ fn ^ " " ^ (string_of_int (List.length in_vars))
......@@ -358,18 +357,25 @@ typedef float _float;
flush oc;
close_out oc
let var_to_rif_type var =
match Var.typ var with
| Type.BoolT -> "bool"
| Type.IntT -> "int"
| Type.FloatT -> "real"
| Type.UT _ -> assert false
let var_to_format_print var =
match Var.typ var with
| Type.BoolT -> "%d"
| Type.IntT -> "%d"
| Type.FloatT -> "%lf"
| Type.FloatT -> "%lf" (* XXX ??? *)
| Type.UT _ -> assert false
let var_to_format_scan var =
match Var.typ var with
| Type.BoolT -> "%c"
| Type.IntT -> "%d"
| Type.FloatT -> "%lf"
| Type.FloatT -> "%lf" (* XXX ??? *)
| Type.UT _ -> assert false
let var_to_cast var =
......@@ -398,13 +404,54 @@ let put_socket_func put fn in_vars out_vars loc_vars =
#include <netinet/in.h>
#include <netdb.h>
#endif
" ^ (if option.gen_mode = Alices then
"#include \"Ims/ImsMessageStack.h\""
else "")
^
"
#ifdef _DEBUG
#define dbg_printf(...) fprintf(fp, __VA_ARGS__); fflush(fp)
#else
#define dbg_printf(...) while(0)
#endif
void raise_info(const char* msg)
{
ImsMessageStack xMessageStack ;
xMessageStack.InsertErrorMessage(\"0\", \"Err\" , cImsInfoAlone, IMS_DEBUG_INFO(Null))
<< \"Lurette/Alices interface: %0\"
<< msg ;
throw xMessageStack ;
}
void raise_warning(const char* msg)
{
ImsMessageStack xMessageStack ;
xMessageStack.InsertErrorMessage(\"0\", \"Err\" , cImsWarning, IMS_DEBUG_INFO(Null))
<< \"Lurette/Alices interface: %0\"
<< msg ;
throw xMessageStack ;
}
void raise_error(const char* msg)
{
ImsMessageStack xMessageStack ;
xMessageStack.InsertErrorMessage(\"0\", \"Err\" , cImsError, IMS_DEBUG_INFO(Null))
<< \"Lurette/Alices interface: %0\"
<< msg ;
throw xMessageStack ;
}
void raise_fatal_error(const char* msg)
{
ImsMessageStack xMessageStack ;
xMessageStack.InsertErrorMessage(\"0\", \"Err\" , cImsFatal, IMS_DEBUG_INFO(Null))
<< \"Lurette/Alices interface: %0\"
<< msg ;
throw xMessageStack ;
}
/*--------
Output procedures must be defined,
Input procedures must be used:
......@@ -432,75 +479,50 @@ launch the lutin interpreter and init socket stuff
int newsockfd;
int portno;
int clilen;
int rc;
#ifndef _WIN32
int lutin_pid;
#endif
struct sockaddr_in serv_addr;
struct sockaddr_in cli_addr;
char portno_str[10];
char buff[MAX_BUFF_SIZE_4];
char *sock_addr = \""^option.sock_addr^"\";
const char *args[] = {
#ifdef _WIN32
\"call-via-socket.exe\", -addr, sock_addr, -port, portno_str, -server, \""^(String.escaped lutin)^"\",
#else
\"call-via-socket\", -addr, sock_addr, -port, portno_str, -server, \""^(String.escaped lutin)^"\",
#endif
" ^ (match option.main_node with None -> "" | Some node -> ("\"-main\", \""^node^"\", "))
^ (match option.seed with None -> "" | Some i -> ("\"-seed\", \""^(string_of_int i)^"\", "))
^ (if option.boot then "\"-boot\", " else "")
^ (if option.load_mem then "\"--load-mem\", " else "")
^ (match option.oracle_ec with Some f -> "\"--oracle-ec\", \"" ^ (String.escaped f) ^ "\", " | None -> "")
^ (match option.precision with None -> "" | Some i -> ("\"-precision\", \""^(string_of_int i)^"\", "))
^" \""^ (String.escaped lut_file) ^"\", \"-rif\",\""^(
match option.rif with
Some rif -> String.escaped rif
| None -> String.escaped (fn^".rif"))
^"\", NULL};
// Socket administration stuff
#ifdef _WINSOCK
WSADATA WSAData;
WSAStartup(MAKEWORD(2,0), &WSAData);
#endif
ctx = malloc(sizeof("^ fn ^ "_ctx));
dbg_printf(\"malloc\");
ctx = ("^ fn ^ "_ctx*) malloc(sizeof("^ fn ^ "_ctx));
ctx->client_data = cdata;
ctx->step_number = 0;
dbg_printf(\"setlocale\\n\");
setlocale(LC_ALL, \"English\");
dbg_printf(\"opening socket\\n\");
sockfd = socket(AF_INET, SOCK_STREAM, 0);
if (sockfd < 0) printf(\"Error: opening socket\");
serv_addr.sin_family = AF_INET;
serv_addr.sin_addr.s_addr = inet_addr(sock_addr);
portno = 2000;
dbg_printf(\"Try Binding %s:%d...\\n\",sock_addr,portno);
serv_addr.sin_port = htons(portno);
while (bind(sockfd, (struct sockaddr *) &serv_addr, sizeof(serv_addr)) ) {
portno++;
dbg_printf(\"Binding %s:%d...\\n\",sock_addr,portno);
serv_addr.sin_port = htons(portno);
if (portno > 4000) { printf(\"Error: cannot bind socket\\n\"); exit(2); }
};
if (portno > 4000) {
raise_error(\"" ^ fn ^ ": cannot find a free socket port\");
}
};
dbg_printf(\"Binding %s:%d...\\n\",sock_addr,portno);
sprintf(portno_str, \"%d\", portno);
#ifndef _LAUNCH_LUTIN_AUTOMATICALLY
printf(\" >>> Waiting for lutin to connect on %s:%s\\n\", sock_addr, portno_str);
#else
dbg_printf(\"Forking...%d\\n\",portno);
#ifdef _WIN32
_spawnvp(_P_DETACH, args[0], args);
#else
lutin_pid = fork();
if(lutin_pid == 0) {
execvp(args[0], args);
printf(\"Unknown command\\n\");
return 0;
}
#endif
#endif
printf(msg,\" Waiting for lurette to connect on %s:%s\\n\", sock_addr, portno_str);
//raise_info(msg);
dbg_printf(\"Waiting for lurette to connect\\n\");
dbg_printf(\"Listening...\\n\");
listen(sockfd,5);
......@@ -509,15 +531,8 @@ launch the lutin interpreter and init socket stuff
newsockfd = accept(sockfd, (struct sockaddr *) &cli_addr, &clilen);
if (newsockfd < 0) printf(\"Error: on accept\");
ctx->sock = newsockfd;
rc = recv(ctx->sock, buff, MAX_BUFF_SIZE_4, 0);
if (rc<0) { printf(\"Error: cannot read on socket\\n\"); exit(2); }
dbg_printf(\"Skipping '%s'\\n\", ctx->buff);
memset(ctx->buff, 0, MAX_BUFF_SIZE);
#ifndef _WIN32
ctx->lp = lutin_pid;
#endif
return ctx;
}
......@@ -541,23 +556,44 @@ let char_decl =
(String.concat "" (List.rev (List.fold_left decl_char [] out_vars)))
in
let var_to_adress var ="ctx->_" ^ (Var.name var) in
let all_vars = in_vars @ out_vars in
(if !cpt = 0 then "" else char_decl) ^
(if option.load_mem then " if (ctx->step_number == 0) {
(
(* if option.load_mem then *)
" if (ctx->step_number == 0) {
sprintf(ctx->buff, \"#inputs "^(
List.fold_left
(fun acc var -> acc ^ "\\\""^ (Var.name var) ^ "\\\":" ^ (var_to_rif_type var) ^ " ")
""
out_vars) ^"\\n\");
dbg_printf(\"\\n\\n ---- Sending the Alices input decl: '%s'\\\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
sprintf(ctx->buff, \"#outputs "^(
List.fold_left
(fun acc var -> acc ^ "\\\""^ (Var.name var) ^ "\\\":" ^ (var_to_rif_type var) ^ " ")
""
in_vars) ^"\\n\");
dbg_printf(\"\\n\\n ---- Sending the Alices output decl: '%s'\\\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
sprintf(ctx->buff, \""^(
List.fold_left
(fun acc var -> acc ^ (var_to_format_print var) ^ " ")
""
out_vars) ^"\\n\", "
all_vars) ^"\\n\", "
^
(List.fold_left
(fun acc var -> acc ^ ", "^ (var_to_adress var))
(var_to_adress (List.hd out_vars))
((List.tl out_vars)))
(var_to_adress (List.hd all_vars))
((List.tl all_vars)))
^
");
dbg_printf(\"\\n\\n ---- Sending lutin memories: '%s'\\n\",ctx->buff);
dbg_printf(\"\\n\\n ---- Sending the 'cliché': '%s'\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
}; " else "") ^
};
") ^
(if option.boot then " if (ctx->step_number > 0) {
" else "
") ^
......@@ -574,16 +610,22 @@ let var_to_adress var ="ctx->_" ^ (Var.name var) in
((List.tl in_vars)))
^
");
dbg_printf(\"\\n\\n ---- A new Step begins. Sending to sock: '%s'\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
")^ (if option.boot then "} " else "") ^ "
dbg_printf(\"\\n\\n ---- A new Step begins. Sending to sock: '%s'\\n\",ctx->buff);
send(ctx->sock, ctx->buff, (int) strlen(ctx->buff),0);
")^
(if option.boot then "} " else "") ^ "
dbg_printf(\"reading inputs\\n\");
rc = 0;
rc = recv(ctx->sock, ctx->buff, MAX_BUFF_SIZE, 0);
if (rc<0) { printf(\"Error: cannot read on socket\\n\"); exit(2); }
dbg_printf(\"reading '%s'\\n\",ctx->buff);
sscanf(ctx->buff, \"" ^
if (rc<0) {
printf(\"Error: cannot read on socket\\n\");
raise_error(\"" ^ fn ^ ": cannot read on socket\");
};
dbg_printf(\"reading '%s'\\n\",ctx->buff);
sscanf(ctx->buff, \"" ^
let cpt = ref 0 in
let var_to_adress var =
if (Var.typ var= Type.BoolT) then (
......@@ -659,13 +701,16 @@ void " ^ fn ^ "_reset(" ^ fn ^ "_ctx* ctx){
let (gen_c_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit) =
let (gen_c_file : string -> Exp.var list -> Exp.var list -> Exp.var list -> unit) =
fun fn in_vars out_vars loc_vars ->
let oc =
if option.gen_mode = Scade then
my_open_out (Filename.concat option.output_dir (fn ^ "_fctext.c"))
else
my_open_out (Filename.concat option.output_dir (fn ^ ".c"))
match option.gen_mode with
Scade ->
my_open_out (Filename.concat option.output_dir (fn ^ "_fctext.c"))
| Alices ->
my_open_out (Filename.concat option.output_dir (fn ^ ".cpp"))
| _ ->
my_open_out (Filename.concat option.output_dir (fn ^ ".c"))
in
let put s = output_string oc s in
let putln s = output_string oc (s^"\n") in
......@@ -906,7 +951,7 @@ let (main : unit -> unit) =
(List.map var_to_vn_ct state.s.in_vars)
(List.map var_to_vn_ct state.s.out_vars)
| Scade -> ()
| Alice ->
| Alices ->
let alice_args = {
Luc2alice.env_name = fn;
Luc2alice.alice_module_name = option.calling_module_name ;
......
......@@ -15,7 +15,7 @@
(* To specify the different C backends (not all the tools have the
same convention for interfacing via C). *)
type gen_mode = Lustre | Scade | Alice | Luciole | Nop
type gen_mode = Lustre | Scade | Alices | Luciole | Nop
type step_mode = Inside | Edges | Vertices
......
......@@ -37,6 +37,8 @@ USE_CAMLP4 = yes
SOURCES = $(LUTIN_SOURCES) \
$(OBJDIR)/ltopArg.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/ocaml.mli \
$(OBJDIR)/ocaml.ml \
$(OBJDIR)/extTools.mli \
......
......@@ -218,7 +218,10 @@ let (gnuplot: string -> bool) =
false
)
else
let gnuplotrif = Unix.getenv "GNUPLOTRIF" in
let gnuplotrif =
try Unix.getenv "GNUPLOTRIF"
with Not_found -> "gnuplot-rif"
in
let cmd2 = ("\n load \"" ^ (Filename.chop_extension file) ^ ".plot\"") in
let res =
......@@ -237,10 +240,6 @@ let (gnuplot: string -> bool) =
);
res
with
Not_found ->
output_string args.ocr "*** Can not find GNUPLOTRIF env variable.\n";
flush args.ocr;
false
| _ ->
false
......@@ -269,7 +268,10 @@ let (quit_gnuplot : unit -> unit) =
let (gnuplot_ps: string -> bool) =
fun file ->
try
let gnuplotrif = Unix.getenv "GNUPLOTRIF" in
let gnuplotrif =
try Unix.getenv "GNUPLOTRIF"
with Not_found -> "gnuplot-rif"
in
let res = my_create_process gnuplotrif [file; "-cps"]
stdin args.ocr args.ecr
in
......@@ -281,10 +283,6 @@ let (gnuplot_ps: string -> bool) =
res
with
Not_found ->
output_string args.ocr "*** Can not find GNUPLOTRIF env variable.\n";
flush args.ocr;
false
| _ ->
false
......@@ -31,8 +31,10 @@ type program_kind = SUT | Env | Oracle | PK_error of string
type reactive_program =
| LustreV4 of string * string
| LustreV6 of string * string
| LustreEc of string
| Lutin of string * string
| Socket of string * int
| SocketInit of string * int
let program_kind_of_string = function
| "sut" -> SUT
......@@ -49,8 +51,10 @@ let program_kind_to_string = function
let reactive_program_to_string = function
| LustreV4(f,node) -> "v4:"^f^":"^node
| LustreV6(f,node) -> "v6:"^f^":"^node
| LustreEc(f) -> "ec:"^f^":"
| Lutin(f,node) -> "lutin:"^f^":"^node
| Socket(addr,port) -> "socket:"^addr^":"^(string_of_int port)
| SocketInit(addr,port) -> "socket_init:"^addr^":"^(string_of_int port)
type t = {
......@@ -84,6 +88,7 @@ type t = {
mutable step_mode : step_mode;
mutable luciole_mode : bool;
mutable delay_env_outputs : bool;
mutable step_by_step : int option ;
mutable display_local_var : bool ;
......@@ -158,6 +163,7 @@ let (args : t) = {
all_vertices = false ;
step_mode = Inside ;
luciole_mode = false;
delay_env_outputs = false;
step_by_step = None ;
show_step = false ;
display_local_var = true ;
......@@ -311,8 +317,10 @@ let (parse_rp_string : string -> unit) =
match List.tl l with
| ["lutin"; prog; node] -> Lutin(prog, node)
| ["v6"; prog; node] -> LustreV6(prog, node)
| ["ec"; prog] -> LustreEc(prog)
| ["v4"; prog; node] -> LustreV4(prog, node)
| ["socket"; addr; port] -> Socket(addr, int_of_string port)
| ["socket_init"; addr; port] -> SocketInit(addr, int_of_string port)
| _ -> failwith ("Unsupported kind of reactive program:"^str)
in
match program_kind_of_string (List.hd l) with
......@@ -634,6 +642,9 @@ let rec speclist =
),
"\t\tSet the step mode used to perform the step.\n";
"--delay-env-outputs", Arg.Unit (fun _ -> args.delay_env_outputs <- true),
"\t Delay the outputs of the environements before transmitting them to the oracles.";
"--luciole", Arg.Unit (fun _ -> args.luciole_mode <- true),
"\t Call lurette via luciole.";
......
......@@ -47,66 +47,58 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int) =
)
let (f : LtopArg.t -> int) =
fun args ->
(* Get sut info (var names, step func, etc.) *)
let _ =
print_string "\nRun direct mode !!! \n";
flush stdout;
in
let sut_in, sut_out, sut_kill, sut_step_sl =
let add_init init (a,b,c,d) = (a,b,c,d,init,init) in
let sut_in, sut_out, sut_kill, sut_step_sl, sut_init_in, sut_init_out =
match args.suts with
[LustreV6(prog,node)] -> LustreRun.make_v6 prog node
(* | [Lutin(prog,node)] -> LutExe.make prog node *)
| [Socket(addr, port)] -> LustreRun.make_socket addr port
[LustreV6(prog,node)] -> add_init [] (LustreRun.make_v6 prog node)
| [LustreEc(prog)] -> add_init [] (LustreRun.make_ec prog)
| [Lutin(prog,node)] -> add_init [] (LustreRun.make_lut prog node)
| [Socket(addr, port)] -> add_init [] (LustreRun.make_socket addr port)
| [SocketInit(addr, port)] -> LustreRun.make_socket_init addr port
| _ -> assert false
in
let (to_subst_list : (string * string) list -> Value.OfIdent.t -> Rif_base.subst list) =
fun var_decl vals ->
List.map (fun (n,_) -> n, Value.to_rif_val (Value.OfIdent.get vals n)) var_decl
in
let (to_vals : Rif_base.subst list -> Value.OfIdent.t) =
List.fold_left
(fun acc (n,v) -> Value.OfIdent.add acc (n, Value.from_rif_val v))
Value.OfIdent.empty
in
let sut_step vals = to_vals (sut_step_sl (to_subst_list sut_in vals)) in
let _ =
print_string "Run direct mode: sut loaded \n";
flush stdout;
in
(* Get oracle info (var names, step func, etc.)*)
let oracle_in, oracle_out, oracle_kill, oracle_step_sl =
match args.oracles with
[LustreV6(prog,node)] -> LustreRun.make_v6 prog node
(* | [Lutin(prog,node)] -> LutExe.make prog node *)
| [Socket(addr, port)] -> LustreRun.make_socket addr port
| [LustreEc(prog)] -> LustreRun.make_ec prog
| [LustreV6(prog,node)] -> LustreRun.make_v6 prog node
| [LustreV4(prog,node)] -> assert false (* LustreRun.make_v4 prog node *)
| [Socket(addr, port)] -> LustreRun.make_socket addr port
| [Lutin(prog,node)] -> LustreRun.make_lut prog node
| [SocketInit(addr, port)] -> assert false
| [] -> [],[],(fun () -> ()), (fun _ -> [])
| _ -> assert false
in
let oracle_step vals = (oracle_step_sl (to_subst_list oracle_in vals)) in
let _ =
print_string "Run direct mode: oracle loaded \n";
flush stdout;
in
(* Get env info (var names, step func, etc.) *)
let env_prog =
let env_in, env_out, env_kill, env_step_sl, env_init_in, env_init_out =
match args.envs with
| [Lutin(prog,node)] -> LutExe.make prog node
(* | [LustreV6(prog,node)] -> LustreRun.make_v6 prog node *)
(* | [Socket(addr, port)] -> LustreRun.make_socket addr port *)
| [Lutin(prog,node)] -> add_init [] (LustreRun.make_lut prog node)
| [LustreV6(prog,node)] -> add_init [] (LustreRun.make_v6 prog node)
| [LustreEc(prog)] -> add_init [] (LustreRun.make_ec prog)
| [Socket(addr, port)] -> add_init [] (LustreRun.make_socket addr port)
| [SocketInit(addr, port)] -> LustreRun.make_socket_init addr port
| _ -> assert false
in
let (var_to_string_pair: Exp.var -> string * string) =
fun v -> Var.name v, Type.to_string2 (Var.typ v)
let vars_to_string l =
String.concat "\n" (List.map (fun (vn,vt) -> Printf.sprintf "\t%s:%s" vn vt) l)
in
let env_in = List.map var_to_string_pair (LutExe.in_var_list env_prog) in
let env_out = List.map var_to_string_pair (LutExe.out_var_list env_prog) in
let loc =
if (args.display_local_var) then Some (LutExe.loc_var_list env_prog) else None
let _ = if args.verbose > 0 then
let sut_input_str = vars_to_string sut_in in
let sut_output_str = vars_to_string sut_out in
let env_input_str = vars_to_string env_in in
let env_output_str = vars_to_string env_out in
let oracle_input_str = vars_to_string oracle_in in
let oracle_output_str = vars_to_string oracle_out in
Printf.printf "sut input : \n%s\n" sut_input_str;
Printf.printf "sut output : \n%s\n" sut_output_str;
Printf.printf "env input : \n%s\n" env_input_str;
Printf.printf "env output : \n%s\n" env_output_str;
Printf.printf "oracle input : \n%s\n" oracle_input_str;
Printf.printf "oracle output : \n%s\n" oracle_output_str;
flush stdout
in
let seed =
match args.seed with
......@@ -114,19 +106,64 @@ let (f : LtopArg.t -> int) =
| Some seed -> seed
in
let cov_init =
let is_bool (_,t) = (t = "bool") in
let names = List.filter is_bool (List.tl oracle_out) in
let names = snd (List.split names) in
Coverage.init names args.cov_file args.reset_cov_file
in
let lut_memories = (*
if args.load_mem () then (
output_string oc "#lutin_outputs_memories ";
Rif.read stdin (Some oc) (LutExe.out_var_list env_prog))
else *)
Value.OfIdent.empty
if oracle_out = [] then None else
let is_bool (_,t) = (t = "bool") in
let names = List.filter is_bool (List.tl oracle_out) in
let names = snd (List.split names) in
Some (Coverage.init names args.cov_file args.reset_cov_file)
in
let oc = open_out args.output in