Skip to content

GitLab

Commit ee70bc48 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.65 Fri, 10 May 2002 16:54:24 +0200 by jahier 

Parent-Version:      0.64
Version-Log:

Outputs error message on stderr rather than on stdout.

Project-Description: Lurette
parent 458e1508
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ ee70bc48
......@@ -4,7 +4,7 @@
(test/usager.env 523 1019479246 b/14_usager.env 1.7)
(source/command_line_ima_exe.mli 1045 1020420514 b/34_command_li 1.2)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 13457 1021041152 51_env_state. 1.20)
(source/env_state.ml 13465 1021042464 51_env_state. 1.21)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(bin/Makefile.ima_exe 1926 1020420514 b/41_Makefile.i 1.2)
(source/util.ml 13368 1021041152 35_util.ml 1.20)
......@@ -12,7 +12,7 @@
(source/solver.ml 24560 1017837703 39_solver.ml 1.21)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4388 1019207707 b/20_command_li 1.7)
(source/lurette.ml 11847 1020432102 12_lurette.ml 1.37)
(source/lurette.ml 11959 1021042464 12_lurette.ml 1.38)
(source/solver.mli 1138 1020432102 38_solver.mli 1.11)
(source/env.mli 2077 1020420514 15_env.mli 1.13)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
......@@ -27,10 +27,10 @@
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 908 1020420514 40_parse_env. 1.7)
(source/sim2chro.mli 1429 1017929190 b/23_sim2chro.m 1.4)
(source/ima_exe.ml 9687 1021041152 b/32_ima_exe.ml 1.9)
(source/ima_exe.ml 9703 1021042464 b/32_ima_exe.ml 1.10)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7749 1016803757 49_eval.ml 1.12)
(source/gen_stubs.ml 36477 1020777170 24_generate_l 1.25)
(source/gen_stubs.ml 36621 1021042464 24_generate_l 1.26)
(source/parse_env.ml 18459 1021041152 41_parse_env. 1.19)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/sim2chro.ml 2653 1020777170 b/24_sim2chro.m 1.8)
......
lurette.prj
View file @ ee70bc48
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 64)
(Parent-Version lurette 0 63)
(Project-Version lurette 0 65)
(Parent-Version lurette 0 64)
(Version-Log "
Add support for loop Gauss.
Fix a bug in the handling of loops where lurette (and ima_exe) was
stopping whenever the body of a loop contains no satisfiable formula
whereas the endLoop branch should be taken in that case.
Outputs error message on stderr rather than on stdout.
")
(New-Version-Log "")
(Checkin-Time "Fri, 10 May 2002 16:32:32 +0200")
(Checkin-Time "Fri, 10 May 2002 16:54:24 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -24,14 +20,14 @@ whereas the endLoop branch should be taken in that case.
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.9 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.10 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.3 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.2 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.37 644))
(source/lurette.ml (lurette/12_lurette.ml 1.38 644))
(source/command_line.ml (lurette/b/20_command_li 1.7 644))
(source/command_line.mli (lurette/b/21_command_li 1.6 644))
......@@ -67,7 +63,7 @@ whereas the endLoop branch should be taken in that case.
(source/eval.ml (lurette/49_eval.ml 1.12 644))
(source/env_state.mli (lurette/50_env_state. 1.18 644))
(source/env_state.ml (lurette/51_env_state. 1.20 644))
(source/env_state.ml (lurette/51_env_state. 1.21 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.10 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.12 644))
......@@ -78,7 +74,7 @@ whereas the endLoop branch should be taken in that case.
(source/gne.mli (lurette/b/36_gne.mli 1.1 644))
(source/gne.ml (lurette/b/37_gne.ml 1.1 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.25 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.26 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.12 744))
......
source/env_state.ml
View file @ ee70bc48
......@@ -371,7 +371,7 @@ let (read_env_state_one_file : string -> node) =
Parse_env.parse_automata(
Parse_env.lexer(Stream.of_channel (open_in file)))
with e ->
print_string ("*** Error while parsing the environment file " ^ file ^ "\n");
output_string stderr ("*** Error while parsing the environment file " ^ file ^ "\n");
flush stdout;
raise e
in
......
source/gen_stubs.ml
View file @ ee70bc48
......@@ -229,9 +229,9 @@ let (check_var_type: vn_ct list -> vn_ct list -> vn_ct list -> res) =
in
if (not (sut_vars = or_vi)) then
(
print_string "\n*** sut input and output vars are: ";
output_string stderr "\n*** sut input and output vars are: ";
print_var_list sut_vars;
print_string "\n*** whereas oracle inputs are: ";
output_string stderr "\n*** whereas oracle inputs are: ";
print_var_list or_vi ;
Error("\n*** sut inputs union sut outputs" ^
" should be the same as oracle inputs.\n")
......@@ -244,7 +244,7 @@ let (check_var_type: vn_ct list -> vn_ct list -> vn_ct list -> res) =
)
then
(
print_string "\noracle outputs: ";
output_string stderr "\noracle outputs: ";
print_var_list or_vo ;
Error("\n*** Oracle outputs should be of one variable " ^
"of type boolean.\n")
......@@ -511,20 +511,20 @@ let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_c
if (List.length lin <> List.length sut_in_list)
then
(
print_string "*** \t";
output_string stderr "*** \t";
print_spl lin;
print_string " does not have the same size as :\n\t";
output_string stderr " does not have the same size as :\n\t";
print_sl sut_in_list;
print_string "\n\n"
output_string stderr "\n\n"
);
if (List.length lout <> List.length sut_out_list)
then
(
print_string "*** \t";
output_string stderr "*** \t";
print_spl lout;
print_string " does not have the same size as :\n\t";
output_string stderr " does not have the same size as :\n\t";
print_sl sut_out_list;
print_string "\n\n"
output_string stderr "\n\n"
);
in
(
......@@ -932,7 +932,7 @@ let main2 sut oracle =
then
if ((Sys.command ("echo \"... camlidl -header sut_idl_stub.idl \" ;"
^ " camlidl -header sut_idl_stub.idl ")) <> 0)
then print_string ("*** Can't call camlidl on sut_idl_stub.idl; " ^
then output_string stderr ("*** Can't call camlidl on sut_idl_stub.idl; " ^
"is camlidl in your path? Does sut_idl_stub.idl exist?\n\n")
else print_string " ... ok\n";
......@@ -957,7 +957,7 @@ let c_type_to_lustre_type ct =
then "bool"
else
(
print_string ("*** I don't know that type, sorry. It should work if "
output_string stderr ("*** I don't know that type, sorry. It should work if "
^ "you provide your own oracle however.\n");
flush stdout;
assert false
......@@ -1016,7 +1016,7 @@ let compile_lustre_program_if_needed lustre_prog =
)
then
(
print_string (" ... No " ^ lustre_prog ^ ".c or no " ^ lustre_prog ^
output_string stderr (" ... No " ^ lustre_prog ^ ".c or no " ^ lustre_prog ^
".h exist(s), so I try to compile " ^ lustre_prog ^
".lus with the lustre compiler...\n");
let cmd = ("lustre " ^ lustre_prog ^ ".lus " ^ lustre_prog) in
......@@ -1038,7 +1038,7 @@ let (main : unit -> 'a) =
let arg_nb = (Array.length Sys.argv) - 1 in
if arg_nb = 0
then
print_string usage
output_string stderr usage
else if arg_nb = 1
then
(
......@@ -1058,10 +1058,10 @@ let (main : unit -> 'a) =
(
if ((Sys.command ("lustre always_true.lus always_true")) <> 0)
then failwith "*** lustre compilation failed. Is lustre in your path?\n"
else print_string " ... ok\n";
else output_string stderr " ... ok\n";
if ((Sys.command ("ec2c always_true.ec")) <> 0)
then failwith "*** ec2c failed. Is it in your path?\n"
else print_string " ... ok\n"
else output_string stderr " ... ok\n"
)
);
main2 sut "always_true"
......@@ -1076,10 +1076,10 @@ let (main : unit -> 'a) =
in
main2 sut oracle
with Invalid_argument(_) ->
print_string usage
output_string stderr usage
| Sys_error(errMsg) ->
print_string ("\n*** " ^ errMsg ^ "\n") ;
print_string usage
output_string stderr ("\n*** " ^ errMsg ^ "\n") ;
output_string stderr usage
| ecxp ->
raise ecxp
;;
......
source/ima_exe.ml
View file @ ee70bc48
......@@ -166,11 +166,11 @@ let rec (main : unit -> 'a) =
fun _ ->
try
if (arg_nb < 2)
then print_string usage
then output_string stderr usage
else
main2 ()
with
Failure(errmsg) -> print_string errmsg
Failure(errmsg) -> output_string stderr errmsg
| e -> raise e
and
......
source/lurette.ml
View file @ ee70bc48
......@@ -49,21 +49,21 @@ let (check_var_decl_consistency : (vn * string) list -> (vn * string) list -> un
Env_state.set_output_var_names out_env;
if not(list_are_equals out_env2 in_sut) then
(
print_string "\nenv outputs: ";
output_string stderr "\nenv outputs: ";
Print.vn_str out_env2;
print_string "\nsut inputs: ";
output_string stderr "\nsut inputs: ";
Print.vn_str in_sut;
print_string "\n*** env outputs and sut inputs should be the same.\n";
output_string stderr "\n*** env outputs and sut inputs should be the same.\n";
flush stdout ;
assert false
)
else if not(list_are_equals in_env2 out_sut) then
(
print_string "\nenv inputs: ";
output_string stderr "\nenv inputs: ";
Print.vn_str in_env2;
print_string "\nsut outputs: ";
output_string stderr "\nsut outputs: ";
Print.vn_str out_sut;
print_string "\n*** env inputs and sut outputs should be the same.\n";
output_string stderr "\n*** env inputs and sut outputs should be the same.\n";
flush stdout ;
assert false
)
......@@ -83,7 +83,7 @@ external random_seed: unit -> int = "sys_random_seed";;
let rec (main : unit -> 'a) =
fun _ ->
try
if (arg_nb < 5) then print_string usage
if (arg_nb < 5) then output_string stderr usage
else
let s = (cmd_line_string_to_int Sys.argv.(1)
"*** int expected as first argument." )
......@@ -98,7 +98,7 @@ let rec (main : unit -> 'a) =
else () ;
res
with
Failure(errmsg) -> print_string errmsg
Failure(errmsg) -> output_string stderr errmsg
| e -> raise e
and
......@@ -284,22 +284,22 @@ and
if (List.mem false results)
then (
print_string ("*** An assertion of the oracle has been violated" ^
output_string stderr ("*** An assertion of the oracle has been violated" ^
" at time " ^ (string_of_int t) ^
" with the following values:\n ");
print_string "\n*** sut inputs names and types:" ;
output_string stderr "\n*** sut inputs names and types:" ;
Print.vn_str Lurette_stub.sut_input_var_name_and_type_list;
print_string "\n*** sut outputs names and types: " ;
output_string stderr "\n*** sut outputs names and types: " ;
Print.vn_str Lurette_stub.sut_output_var_name_and_type_list;
print_string "\n***" ;
output_string stderr "\n***" ;
Util.list_iter3
(fun i o r ->
if (not r) then
(
print_string "\n*** sut inputs:" ;
output_string stderr "\n*** sut inputs:" ;
print_subst_list i stdout;
print_string " sut outputs: " ;
output_string stderr " sut outputs: " ;
print_env_in o stdout
)
else
......
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