Commit 62b3fe18 authored by erwan's avatar erwan

New: remove all stuff that was here for sentimental reasons (old lurette toplevel)

nb:there is now no more dependency on camlp4!
parent 098a10d1
Pipeline #28150 passed with stages
in 8 minutes and 39 seconds
...@@ -26,7 +26,7 @@ SourceRepository "master" ...@@ -26,7 +26,7 @@ SourceRepository "master"
Executable lutin Executable lutin
Path: lutin/src Path: lutin/src
MainIs: main.ml MainIs: main.ml
BuildDepends: str,unix,num,rdbg-plugin (>= 1.177),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp BuildDepends: str,unix,num,rdbg-plugin (>= 1.177),lutin-utils,ezdl,gbddml,polka,camlidl,gmp
NativeOpt: -w A -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind? NativeOpt: -w A -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Build: true Build: true
Install:true Install:true
...@@ -36,7 +36,7 @@ Executable lutin ...@@ -36,7 +36,7 @@ Executable lutin
Executable "lutin.dbg" Executable "lutin.dbg"
Path: lutin/src Path: lutin/src
MainIs: main.ml MainIs: main.ml
BuildDepends: str,unix,num,rdbg-plugin (>= 1.177),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp BuildDepends: str,unix,num,rdbg-plugin (>= 1.177),lutin-utils,ezdl,gbddml,polka,camlidl,gmp
NativeOpt: -w A -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind? NativeOpt: -w A -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Build: true Build: true
Install:false Install:false
...@@ -55,7 +55,7 @@ Library lutin ...@@ -55,7 +55,7 @@ Library lutin
XMETADescription: Provides an API to call Lutin from ocaml (and rdbg) XMETADescription: Provides an API to call Lutin from ocaml (and rdbg)
Path: lutin/src Path: lutin/src
Modules: LutinRun Modules: LutinRun
BuildDepends: camlp4,lutin-utils,ezdl,gbddml,bigarray,polka,camlidl,lutils BuildDepends: lutin-utils,ezdl,gbddml,bigarray,polka,camlidl,lutils
Install:true Install:true
CompiledObject: native CompiledObject: native
XMETAEnable: true XMETAEnable: true
...@@ -66,7 +66,7 @@ Library bddrand ...@@ -66,7 +66,7 @@ Library bddrand
XMETADescription: A simple front-end to the lutin Random toss machinary XMETADescription: A simple front-end to the lutin Random toss machinary
Path: lutin/src Path: lutin/src
Modules: BddRandom,Dimacs Modules: BddRandom,Dimacs
BuildDepends: camlp4,lutin-utils,ezdl,gbddml,bigarray,polka,camlidl,lutils BuildDepends: lutin-utils,ezdl,gbddml,bigarray,polka,camlidl,lutils
FindlibParent: lutin FindlibParent: lutin
Install:true Install:true
CompiledObject: native CompiledObject: native
...@@ -79,7 +79,7 @@ Library bddrand ...@@ -79,7 +79,7 @@ Library bddrand
# Path: lutin/src # Path: lutin/src
# Modules: Lut4c # Modules: Lut4c
# FindlibParent: lutin # FindlibParent: lutin
# BuildDepends: str,unix,num,rdbg-plugin (>= 1.51),lutin-utils,ezdl,gbddml,polka,camlp4 # BuildDepends: str,unix,num,rdbg-plugin (>= 1.51),lutin-utils,ezdl,gbddml,polka
# Install: true # Install: true
# CSources: lut4c_stubs.h,lut4c_stubs.c # CSources: lut4c_stubs.h,lut4c_stubs.c
# CCOpt: -fPIC # CCOpt: -fPIC
...@@ -97,25 +97,13 @@ Library "lutin-utils" ...@@ -97,25 +97,13 @@ Library "lutin-utils"
Executable lurette Executable lurette
Path: lurette-nocaml/src Path: lurette-nocaml/src
MainIs: lurette.ml MainIs: lurette.ml
BuildDepends: str,unix,num,dynlink,extlib,camlp4,lutils (>= 1.9),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp,rdbg-plugin (>= 1.177),lustre-v6,lutin BuildDepends: str,unix,num,dynlink,extlib,lutils (>= 1.9),lutin-utils,ezdl,gbddml,polka,camlp4,camlidl,gmp,rdbg-plugin (>= 1.177),lustre-v6,lutin
NativeOpt: rdbg4lurette.cmxa # for some reasons not recognized as a package NativeOpt: rdbg4lurette.cmxa # for some reasons not recognized as a package
Install:true Install:true
CompiledObject: native CompiledObject: native
Install: true Install: true
CClib: -lcamlidl CClib: -lcamlidl
# The old lurette. Remove ?
# it create a weird dependancies on lustre-v6
Executable lurette_old
Path: ltop/src
MainIs: lurettetop.ml
BuildDepends: num,str,unix,dynlink,lustre-v6,lutin,ezdl,gbddml,polka,camlp4,camlidl
Build: true
NativeOpt: -package dynlink # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Install:true
CompiledObject: native
CClib: -lcamlidl
CCOpt: -fPIC
# should be moved to lutils # should be moved to lutils
Library ezdl Library ezdl
...@@ -153,26 +141,6 @@ Library polka ...@@ -153,26 +141,6 @@ Library polka
DllLib: libgmp.so dllcamlidl.so DllLib: libgmp.so dllcamlidl.so
# should be part of rdbg?
Executable "check-rif"
Path: ltop/src
MainIs: checkRif.ml
BuildDepends: num,str,unix,lutils,ezdl,lustre-v6
NativeOpt: -package num # XXX turn around a bug in oasis/ocamlbuild/ocamlfind?
Build: true
Install:true
CompiledObject: native
CCOpt: -fPIC
Executable "call-via-socket"
Path: ltop/src
MainIs: call_via_socket.ml
BuildDepends: str,unix
Build: true
Install:true
CompiledObject: native
# XXX not working # XXX not working
Document "lutin-man.pdf" Document "lutin-man.pdf"
Title: Lutin language reference manual Title: Lutin language reference manual
......
# OASIS_START # OASIS_START
# DO NOT EDIT (digest: e206596fa32c72a65d0b3f6b19835f56) # DO NOT EDIT (digest: c6eb218d44c657361aeca44a19f21c63)
# Ignore VCS directories, you can use the same kind of rule outside # Ignore VCS directories, you can use the same kind of rule outside
# OASIS_START/STOP if you want to exclude directories that contains # OASIS_START/STOP if you want to exclude directories that contains
# useless stuff for the build process # useless stuff for the build process
...@@ -89,35 +89,6 @@ true: annot, bin_annot ...@@ -89,35 +89,6 @@ true: annot, bin_annot
"lutin/src/lutin.cmxa": oasis_library_lutin_dlllib "lutin/src/lutin.cmxa": oasis_library_lutin_dlllib
<lutin/src/*.ml{,i,y}>: package(bigarray) <lutin/src/*.ml{,i,y}>: package(bigarray)
<lutin/src/*.ml{,i,y}>: package(lutils) <lutin/src/*.ml{,i,y}>: package(lutils)
# Executable lurette_old
<ltop/src/*.ml{,i,y}>: oasis_executable_lurette_old_ccopt
"ltop/src/lurettetop.native": oasis_executable_lurette_old_cclib
"ltop/src/lurettetop.native": oasis_executable_lurette_old_native
<ltop/src/*.ml{,i,y}>: oasis_executable_lurette_old_native
"ltop/src/lurettetop.native": package(bigarray)
"ltop/src/lurettetop.native": package(camlidl)
"ltop/src/lurettetop.native": package(camlp4)
"ltop/src/lurettetop.native": package(dynlink)
"ltop/src/lurettetop.native": package(gmp)
"ltop/src/lurettetop.native": package(lustre-v6)
"ltop/src/lurettetop.native": package(lutils)
"ltop/src/lurettetop.native": package(num)
"ltop/src/lurettetop.native": package(str)
"ltop/src/lurettetop.native": package(unix)
"ltop/src/lurettetop.native": use_ezdl
"ltop/src/lurettetop.native": use_gbddml
"ltop/src/lurettetop.native": use_lutin
"ltop/src/lurettetop.native": use_lutin-utils
"ltop/src/lurettetop.native": use_polka
<ltop/src/*.ml{,i,y}>: package(bigarray)
<ltop/src/*.ml{,i,y}>: package(camlidl)
<ltop/src/*.ml{,i,y}>: package(camlp4)
<ltop/src/*.ml{,i,y}>: package(dynlink)
<ltop/src/*.ml{,i,y}>: package(gmp)
<ltop/src/*.ml{,i,y}>: use_gbddml
<ltop/src/*.ml{,i,y}>: use_lutin
<ltop/src/*.ml{,i,y}>: use_lutin-utils
<ltop/src/*.ml{,i,y}>: use_polka
# Executable lurette # Executable lurette
"lurette-nocaml/src/lurette.native": oasis_executable_lurette_cclib "lurette-nocaml/src/lurette.native": oasis_executable_lurette_cclib
"lurette-nocaml/src/lurette.native": oasis_executable_lurette_native "lurette-nocaml/src/lurette.native": oasis_executable_lurette_native
...@@ -161,7 +132,6 @@ true: annot, bin_annot ...@@ -161,7 +132,6 @@ true: annot, bin_annot
"lutin/src/main.byte": oasis_executable_lutin_dbg_native "lutin/src/main.byte": oasis_executable_lutin_dbg_native
<lutin/src/*.ml{,i,y}>: oasis_executable_lutin_dbg_native <lutin/src/*.ml{,i,y}>: oasis_executable_lutin_dbg_native
"lutin/src/main.byte": package(camlidl) "lutin/src/main.byte": package(camlidl)
"lutin/src/main.byte": package(camlp4)
"lutin/src/main.byte": package(gmp) "lutin/src/main.byte": package(gmp)
"lutin/src/main.byte": package(num) "lutin/src/main.byte": package(num)
"lutin/src/main.byte": package(rdbg-plugin) "lutin/src/main.byte": package(rdbg-plugin)
...@@ -176,7 +146,6 @@ true: annot, bin_annot ...@@ -176,7 +146,6 @@ true: annot, bin_annot
"lutin/src/main.native": oasis_executable_lutin_native "lutin/src/main.native": oasis_executable_lutin_native
<lutin/src/*.ml{,i,y}>: oasis_executable_lutin_native <lutin/src/*.ml{,i,y}>: oasis_executable_lutin_native
"lutin/src/main.native": package(camlidl) "lutin/src/main.native": package(camlidl)
"lutin/src/main.native": package(camlp4)
"lutin/src/main.native": package(gmp) "lutin/src/main.native": package(gmp)
"lutin/src/main.native": package(num) "lutin/src/main.native": package(num)
"lutin/src/main.native": package(rdbg-plugin) "lutin/src/main.native": package(rdbg-plugin)
...@@ -187,7 +156,6 @@ true: annot, bin_annot ...@@ -187,7 +156,6 @@ true: annot, bin_annot
"lutin/src/main.native": use_lutin-utils "lutin/src/main.native": use_lutin-utils
"lutin/src/main.native": use_polka "lutin/src/main.native": use_polka
<lutin/src/*.ml{,i,y}>: package(camlidl) <lutin/src/*.ml{,i,y}>: package(camlidl)
<lutin/src/*.ml{,i,y}>: package(camlp4)
<lutin/src/*.ml{,i,y}>: package(gmp) <lutin/src/*.ml{,i,y}>: package(gmp)
<lutin/src/*.ml{,i,y}>: package(num) <lutin/src/*.ml{,i,y}>: package(num)
<lutin/src/*.ml{,i,y}>: package(rdbg-plugin) <lutin/src/*.ml{,i,y}>: package(rdbg-plugin)
...@@ -197,25 +165,6 @@ true: annot, bin_annot ...@@ -197,25 +165,6 @@ true: annot, bin_annot
<lutin/src/*.ml{,i,y}>: use_gbddml <lutin/src/*.ml{,i,y}>: use_gbddml
<lutin/src/*.ml{,i,y}>: use_lutin-utils <lutin/src/*.ml{,i,y}>: use_lutin-utils
<lutin/src/*.ml{,i,y}>: use_polka <lutin/src/*.ml{,i,y}>: use_polka
# Executable check-rif
<ltop/src/*.ml{,i,y}>: oasis_executable_check_rif_ccopt
"ltop/src/checkRif.native": oasis_executable_check_rif_native
<ltop/src/*.ml{,i,y}>: oasis_executable_check_rif_native
"ltop/src/checkRif.native": package(lustre-v6)
"ltop/src/checkRif.native": package(lutils)
"ltop/src/checkRif.native": package(num)
"ltop/src/checkRif.native": package(str)
"ltop/src/checkRif.native": package(unix)
"ltop/src/checkRif.native": use_ezdl
<ltop/src/*.ml{,i,y}>: package(lustre-v6)
<ltop/src/*.ml{,i,y}>: package(lutils)
<ltop/src/*.ml{,i,y}>: package(num)
<ltop/src/*.ml{,i,y}>: use_ezdl
# Executable call-via-socket
"ltop/src/call_via_socket.native": package(str)
"ltop/src/call_via_socket.native": package(unix)
<ltop/src/*.ml{,i,y}>: package(str)
<ltop/src/*.ml{,i,y}>: package(unix)
# OASIS_STOP # OASIS_STOP
"ltop/src/cmd.ml": syntax_camlp4o "ltop/src/cmd.ml": syntax_camlp4o
#"lutin/src/lut4c.ml": output_obj #"lutin/src/lut4c.ml": output_obj
......
The old lurette top-level (now part of rdbg)
open LtopArg
(* Under the scade GUI, the file config_types.h is automatically
generated. Therefore, i mimick that behavior in the Scade
non GUI mode. *)
let check_config_types_exist args =
let dir = args.tmp_dir in
if
args.sut_compiler = Scade
&& not (Sys.file_exists (Filename.concat dir "config_types.h"))
then
let oc = open_out (Filename.concat dir "config_types.h") in
output_string oc "#define false 0\n";
output_string oc "#define true 1\n";
output_string oc "#define bool int\n";
output_string oc "#define _int int\n";
output_string oc "#define real double\n";
flush oc;
close_out oc
let chop_ext = Util.chop_ext_no_excp
(* XXX bien compliqué tout ca. A reprendre proprement *)
let (f : LtopArg.t -> bool) =
fun args ->
if args.sut_compiler = Stdin || args.direct_mode then true else
let sut_path = Filename.concat args.sut_dir args.sut in
let _ =
check_config_types_exist args;
output_string args.ecr (
"... generating lurette" ^ " from " ^ sut_path ^ "\n");
in
if not (Sys.file_exists sut_path) then (
output_string args.ocr ("\n*** File "^sut_path^" does not exist.\n");
flush args.ocr;
false
)
else (
output_string args.ecr " building lurette ...\n";
flush args.ecr;
if args.sut = "" then (
output_string args.ocr "*** The sut field must be filled in.\n ";
flush args.ecr;
false
)
else
let (oracle, oracle2, oracle_dir) =
match args.oracle
with
| None -> ( "", "",args.tmp_dir)
| Some str ->
let str2 =
if Filename.is_implicit str then
(* we assume the oracle is in the same dir as the
sut in that case *)
(Filename.concat args.sut_dir str)
else
str
in
(str2, str2, args.tmp_dir)
in
let make_rule = "nc" in
let make_opt =
match (args.sut_compiler, args.oracle_compiler) with
| Scade, _ -> "scade"
| VerimagV4, VerimagV6 -> make_rule
| VerimagV6, VerimagV4 -> make_rule
| VerimagV6, VerimagV6 -> make_rule
| VerimagV4, VerimagV4 -> make_rule
| Ocamlopt, Ocamlopt -> "ocaml"
| Sildex, VerimagV4 -> "sildex_sut"
| VerimagV4, Sildex -> "sildex_oracle"
| Sildex, Sildex -> "sildex_both"
| ScadeGUI, _ -> "lurette"
| _, ScadeGUI -> assert false
| _, Scade -> "scade"
| Stdin, _ -> assert false
| _, Stdin -> assert false
| sc,oc ->
assert false
in
if (oracle2 <> "") && not (Sys.file_exists oracle2) then (
output_string args.ocr
("\n*** File " ^ oracle2 ^ " does not exist.\n");
flush args.ocr;
false
)
else (
let sut_node = args.sut_node in
let oracle_node = args.oracle_node in
try
let putenv var value =
Printf.fprintf args.ecr "%s=%s\n" var value;
flush args.ecr;
Unix.putenv var value
in
Unix.chdir args.tmp_dir;
putenv "SUT_DIR" args.tmp_dir;
if args.sut_compiler = Ocamlopt
then putenv "SUT" args.sut
else putenv "SUT" sut_node;
putenv "ENV" args.env;
(match args.pp with None -> () |
Some pp -> putenv "PP" ("-pp "^ (pp)));
putenv "ORACLE_DIR" oracle_dir;
if args.oracle_compiler = Ocamlopt then
(match args.oracle with
None-> ()
| Some str -> putenv "ORACLE" str)
else
putenv "ORACLE" oracle_node;
putenv "USER_TESTING_DIR" (args.sut_dir);
putenv "LURETTE_TMP_DIR" (args.tmp_dir);
if args.sut_compiler = Ocamlopt then (
let ocaml_module =
Filename.basename (chop_ext args.sut) in
let ocaml_module = String.capitalize ocaml_module in
if ocaml_module = "Sut" then
failwith "*** You cannot name your sut 'sut.ml'; please rename it.\n"
else
Ocaml.gen_ocaml_sut ocaml_module
);
(match args.oracle_compiler, args.oracle with
| Ocamlopt, Some oracle ->
let ocaml_module = Filename.basename (chop_ext oracle) in
let ocaml_module = String.capitalize ocaml_module in
if ocaml_module = "Oracle" then
failwith
"*** You cannot name your oracle 'oracle.ml', please rename it.\n"
else
Ocaml.gen_ocaml_oracle ocaml_module
| Ocamlopt, None ->
Ocaml.gen_fake_ocaml_oracle ()
| _,_ -> ()
);
if
if args.sut_compiler <> Ocamlopt then (
not (ExtTools.gen_stubs (Filename.concat args.sut_dir args.sut) sut_node
(if oracle = "" then "" else oracle)
(if oracle = "" then "" else oracle_node)
))
else
false
then
false
else
let make =
try Util2.string_to_string_list (Unix.getenv "MAKE")
with _ ->
["make"]
in
let makefile =
if args.scade_gui then
(Filename.concat args.tmp_dir "Makefile")
else
(Filename.concat
(Filename.concat (ExtTools.lurette_path()) "lib")
"Makefile.lurette")
in
let make_arg_list =
make @
[
"-r";
(* "-C"; *)
(* ("\"" ^ (args.tmp_dir) ^ "\""); *)
"-f";
makefile;
make_opt
]
in
let make_pid =
List.iter
(fun x -> output_string args.ecr (x ^ " ")) make_arg_list;
output_string args.ecr "\n";
flush args.ecr;
Unix.create_process
(List.hd make)
(Array.of_list make_arg_list)
(Unix.stdin)
(Unix.descr_of_out_channel args.ecr)
(Unix.descr_of_out_channel args.ecr)
in
ignore(Unix.waitpid [Unix.WUNTRACED] make_pid);
output_string args.ecr " ... make ok.\n";
flush args.ecr;
true
with
| Unix.Unix_error(error, name, arg) ->
output_string args.ocr
( "*** << " ^
(Unix.error_message error) ^
" >> in the system call: << " ^ name ^ " " ^ arg ^ " >>\n");
flush args.ocr;
false
| Failure e ->
output_string args.ocr e ;
flush args.ocr ;
false
)
)
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the CeCill
** Public License
**-----------------------------------------------------------------------
**
** File: call-via-socket.ml
** Author: erwan.jahier@univ-grenoble-alpes.fr
*)
(* Launch prog and connect its stdin/stdout to sockets *)
let usage = "call-via-socket -addr <inet address> -port <port> [-serveur] \"<prog> <args>\"
Launch prog args connecting its stdin/stdout to a socket and stderr is to a log file.
Fails (with exit code 2) if the port is not available.
"
let client_mode = ref true
let inet_addr = ref (Unix.inet_addr_of_string "127.0.0.1")
let port = ref 2000
let usage_out speclist errmsg =
Printf.printf "%s" (Arg.usage_string speclist errmsg)
let rec speclist =
[
"-addr", Arg.String(fun str -> inet_addr := Unix.inet_addr_of_string str),
"<string>\tSocket inet address (127.0.0.1 by default)";
"-port", Arg.Int(fun str -> port := str),
"<int>\tSocket port (2000 by default)";
"-server", Arg.Unit(fun () -> client_mode := false),
"\tThe prog plays the role of the server (and the role if the client if unset)";
"--help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
"\tDisplay this list of options." ;
"-help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
"";
"-h", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
""
]
(* Parsing command line args *)
let prog, args =
try
let prog = ref "" in
let set_prog str = prog := !prog ^ " " ^ str in
let prog =
Arg.parse speclist set_prog usage;
(Str.split (Str.regexp "[ \t]+") !prog)
in
List.hd prog, Array.of_list prog
with
| Failure(e) -> output_string stdout e; flush_all(); exit 2
| e -> output_string stdout (Printexc.to_string e); flush_all(); exit 2
let log_file = (prog ^ "-via-sockets-stderr.log")
let log = open_out log_file
let _ =
for i = 0 to Array.length Sys.argv -1 do
output_string log (Sys.argv.(i) ^ " ");
done;
output_string log "\n"; flush log;
if Array.length Sys.argv < 3 then (
print_string usage;
flush stdout;
close_out log;
exit 2
)
(*****************************************************************************)
(* Socket administration stuff *)
let sock = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0
let inet_addr = !inet_addr
let inet_addr_str = Unix.string_of_inet_addr inet_addr
let port = !port
let rec connect_loop sock addr k =
try Unix.connect sock addr
with _ ->
if k > 0 then (
output_string log " call-via-socket: connect failed... try once more \n"; flush log;
Unix.sleep 1;
connect_loop sock addr (k-1)
)
else
failwith "call-via-socket: cannot connect to the socket"
let (sock_in, sock_out) =
try
if !client_mode then
(
connect_loop sock (Unix.ADDR_INET(inet_addr, port)) 100 ;
(* connect ne marche que si il y a un accept en attente cot
serveur. Cela entraine une course critique entre le serveur
et le client. Pour y remdier, on essaie 10 fois en attendant
une seconde chaque essai. *)
Printf.fprintf log "call-via-socket: sock connection on %s:%d succeeded " inet_addr_str port;
(Unix.in_channel_of_descr sock, Unix.out_channel_of_descr sock)
)
else
( (* Serveur mode *)
Unix.bind sock (Unix.ADDR_INET(inet_addr, port));
Unix.listen sock 1;
let sock,_ = Unix.accept sock (* bloquant *) in
Printf.fprintf log "call-via-socket -server: sock connection on %s:%d accepted.\n" inet_addr_str port;
(Unix.in_channel_of_descr sock, Unix.out_channel_of_descr sock)
)
with
Unix.Unix_error(errcode, funcstr, paramstr) ->
output_string log "call-via-socket connect failure: ";
output_string log (Unix.error_message errcode);
output_string log ("(" ^ funcstr ^ " " ^ paramstr ^")\n");
flush log;
exit 2
(*****************************************************************************)
(* Forking *)
let pid =
output_string log ("call-via-socket "^prog^":");
output_string log " create child process with '";
for i = 0 to Array.length args -1 do
output_string log (args.(i)^ " ");
done;
output_string log "'\n";
flush log;
Unix.create_process prog args
(Unix.descr_of_in_channel sock_in)
(Unix.descr_of_out_channel sock_out)
(Unix.descr_of_out_channel log)
let _ =
output_string log ("call-via-socket "^prog^": the process creation succeeded.\n");
flush log;
let pid, pstatus = (Unix.waitpid [] pid) in
(* ignore(Unix.wait()); *)
output_string log ("call-via-socket "^prog^":");
(match pstatus with
Unix.WEXITED i -> output_string log (
" the process terminated with exit code " ^ (string_of_int i) ^"\n")
| Unix.WSIGNALED i -> output_string log (
" the process was killed by signal " ^ (string_of_int i) ^"\n")
| Unix.WSTOPPED i -> output_string log (
" the process was stopped by signal " ^ (string_of_int i) ^"\n")
);
output_string log ("call-via-socket "^prog^": bye. \n");
flush log;
close_out log
(*
Se plugger sur l'API c de l'oracle ?
lire le rif sur stdin ?
*)
open Format
(**************************************************************************)
type argT = {
mutable rif : string option;
mutable ec : string;
mutable cov : string;
mutable debug : bool;
mutable reinit_cov : bool;
mutable stop_at_error : bool;
}
let arg = {
rif = None;
ec = "";
cov = "";
debug = false;
reinit_cov = false;
stop_at_error = false;
}
(**************************************************************************)
(* Cloned from the OCaml stdlib Arg module: I want it on stdout! (scrogneugneu) *)
let usage_out speclist errmsg =
Printf.printf "%s" (Arg.usage_string speclist errmsg)
let usage = "Usage: \n\t" ^
Sys.argv.(0) ^ " [options]* -ec <file>.ec <Rif File name to check>
Performs post-mortem oracle checking using ecexe.
The set of oracle Inputs should be included in the set of the RIF
file inputs/outputs.
At the first run, the coverage information is stored/updated in the
coverage file (cf the -cov option to set its name). The variables
declared in this file should be a subset of the oracle outputs. If
the coverage file does not exist, one is is created using all the
oracle outputs. If not all those outputs are meaningfull to compute
the coverage rate, one just need to delete corresponding lines in the
coverage file. The format of the coverage file is straightforward,
but deserves respect.
Options are:
"
let rec speclist =
[
"-ec", Arg.String
(fun str -> arg.ec <- str),
"<string>\tec file name containing the RIF file checker (a.k.a., the oracle)" ;
"-cov", Arg.String
(fun str -> arg.cov <- str),
"<string>\tOverride the default coverage file name (<oracle name>.cov by default).";
"-reset-cov", Arg.Unit (fun _ -> (arg.reinit_cov <- true)),
"\treset the coverage rate (to 0%) before running";
"-stop-at-error", Arg.Unit (fun _ -> (arg.stop_at_error <- true)),
"\tStop processing when the oracle returns false";
"-debug", Arg.Unit (fun _ -> (arg.debug <- true)),
"\tset on the debug mode";
"--help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
"\tDisplay this list of options." ;
"-help", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
"";
"-h", Arg.Unit (fun _ -> (usage_out speclist usage ; exit 0)),
""
]
let _ =
( try Arg.parse speclist (fun str -> arg.rif <- Some str) usage
with
Failure(e) ->
output_string stderr e;
flush stderr;
exit 2
| e ->
output_string stderr (Printexc.to_string e);
flush stderr;
exit 2
);
if arg.ec = "" then (
output_string stderr "*** It is mandatory to set an oracle (cf -ec option)\n";
Arg.usage speclist usage;
flush stderr;
exit 2)
(**************************************************************************)
let rif_ic : in_channel =
match arg.rif with
Some f -> open_in f
| None -> stdin
let rif_in, rif_out = RifIO.read_interface ~label:"check_rif " rif_ic None
let rif_all = rif_in @ rif_out
(**************************************************************************)
(* Oracle launching *)
open RdbgPlugin
let oracle_in, oracle_out, kill_oracle, step_oracle, step_oracle_dbg =