Commit 3764e8b8 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.73 Mon, 29 Jul 2002 13:49:35 +0200 by jahier

Parent-Version:      0.72
Version-Log:

gen_stubs.ml:
sim2chro.ml:
   Do not sort varialble lexicographically but according to
   sut order.

gen_stubs.ml:
   When converting subst list to tuple, do not put fake values
   if the list is empty, but raise a failure (assert false).

   Do not parse idl output to guess the conversion between ml
   and C type but hard code it instead. The rational is that
   I was manually calling camlidl here which was confusing
   make sometimes.

make_lurette:
   exit properly before running lurette whenever something bad
   happen during the make.

Project-Description: Lurette
parent d27d91fe
......@@ -7,19 +7,19 @@
(source/env_state.ml 19663 1027092697 51_env_state. 1.24)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(source/util.ml 13725 1027066799 35_util.ml 1.21)
(source/util.ml 14262 1027943375 35_util.ml 1.23)
(test/time.exp 5583 1027066799 b/48_time.exp 1.1)
(source/solver.ml 24250 1027092697 39_solver.ml 1.24)
(source/solver.ml 24274 1027436332 39_solver.ml 1.25)
(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 11706 1027349504 12_lurette.ml 1.42)
(source/lurette.ml 12222 1027943375 12_lurette.ml 1.43)
(test/temp_int.env 647 1027066799 b/50_temp_int.e 1.1)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/env.mli 2028 1027349504 15_env.mli 1.15)
(test/heater_float.rif.exp 1453 1027066799 b/30_heater_flo 1.3)
(test/heater_float.rif.exp 1453 1027436332 b/30_heater_flo 1.4)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8013 1027349504 16_env.ml 1.29)
(make_lurette 1243 1027066799 27_make_luret 1.13)
(make_lurette 1358 1027943375 27_make_luret 1.15)
(test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 972 1027066799 b/17_passerelle 1.7)
......@@ -27,19 +27,19 @@
(source/rnumsolver.ml 10783 1017837703 b/27_rnumsolver 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1429 1017929190 b/23_sim2chro.m 1.4)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
(source/ima_exe.ml 11851 1027349504 b/32_ima_exe.ml 1.15)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 36621 1021042464 24_generate_l 1.26)
(source/gen_stubs.ml 33500 1027943375 24_generate_l 1.28)
(source/parse_env.ml 22104 1027066799 41_parse_env. 1.20)
(test/temp_float.env 719 1027066799 b/51_temp_float 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
(source/sim2chro.ml 2653 1020777170 b/24_sim2chro.m 1.8)
(source/sim2chro.ml 2720 1027943375 b/24_sim2chro.m 1.10)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3638 1027066799 44_formula.ml 1.14)
(test/time.res 5577 1027349504 b/49_time.res 1.3)
(test/time.res 5576 1027943375 b/49_time.res 1.4)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(test/porte.env 1021 1027066799 b/16_porte.env 1.7)
......@@ -49,11 +49,11 @@
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 24425 1027092697 17_OcamlMakef 1.31)
(OcamlMakefile 25027 1027943375 17_OcamlMakef 1.33)
(source/command_line_ima_exe.ml 2792 1021651153 b/33_command_li 1.4)
(test/ControleurPorte.rif.exp 4756 1027066799 b/29_Controleur 1.5)
(test/ControleurPorte.rif.exp 4756 1027943375 b/29_Controleur 1.7)
(test/tram.env 1038 1027066799 b/15_tram.env 1.7)
(Makefile.lurette 1953 1027066799 b/38_Makefile.l 1.4)
(Makefile.lurette 1960 1027943375 b/38_Makefile.l 1.5)
(source/show_env.ml 3653 1027349504 43_show_env.m 1.11)
(source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
(source/automata.ml 15708 1027349504 b/47_automata.m 1.2)
......@@ -61,7 +61,7 @@
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
(test/Makefile 146 1027066799 c/0_Makefile 1.1)
(test/Makefile 164 1027943375 c/0_Makefile 1.2)
(source/gne.ml 8173 1027066799 b/37_gne.ml 1.2)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
......@@ -69,7 +69,7 @@
(source/print.mli 773 1027066799 46_print.mli 1.10)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 860 1027349504 b/28_heater_int 1.4)
(test/heater_int.rif.exp 860 1027436332 b/28_heater_int 1.5)
(source/formula.ml 7287 1027066799 45_formula.ml 1.16)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/print.ml 5954 1027066799 47_print.ml 1.17)
......
......@@ -39,7 +39,7 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
lurette_stub.ml \
$(PWD)/lurette_stub.ml \
$(LURETTE_PATH)/source/lurette.mli $(LURETTE_PATH)/source/lurette.ml
SOURCES = $(SOURCES_C) \
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.32 Tue, 23 Jul 2002 16:58:52 +0200 jahier $
# $Id: OcamlMakefile 1.33 Mon, 29 Jul 2002 13:49:35 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
......@@ -510,6 +510,13 @@ vroum:
/usr/bin/time -v ./lurette 10000 1 1 tram.env usager.env porte.env \
passerelle.env -seed 1015403953 -ns2c --no-oracle
giro_make:
../../make_lurette onlyroll
giro: giro_make
./lurette 10 1 1 giro.ima
time:
make clean; ../make_lurette ControleurPorte vrai_tram nc; \
\rm -f time.res; touch time.res ; \
......@@ -539,20 +546,24 @@ time:
# Non regression test
test:
../make_lurette ControleurPorte; rm -f tram.rif; touch tram.rif; \
test1:
../make_lurette ControleurPorte; rm -f ControleurPorte.rif; touch ControleurPorte.rif; \
./lurette 100 10 10 -o ControleurPorte.rif tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
diff -u ControleurPorte.rif.exp ControleurPorte.rif > test1.res ;\
\
rm -f test1.res; diff -u ControleurPorte.rif.exp ControleurPorte.rif > test1.res
test2:
../make_lurette heater_int; rm -f heater_int.rif; touch heater_int.rif; \
./lurette 30 10 10 temp_int.env --no-oracle -seed 1013219512 -ns2c -o heater_int.rif ;\
diff -u heater_int.rif.exp heater_int.rif > test2.res ; \
\
rm -f test3.res; diff -u heater_int.rif.exp heater_int.rif > test2.res
test3:
../make_lurette heater_float; rm -f heater_float.rif; touch heater_float.rif; \
./lurette 30 10 10 temp_float.env --no-oracle -seed 1013219512 -ns2c -o heater_float.rif;\
diff -u heater_float.rif.exp heater_float.rif > test3.res ; \
\
ls -l test1.res test2.res test3.res
rm -f test3.res; diff -u heater_float.rif.exp heater_float.rif > test3.res
test: test1 test2 test3
ls -l test1.res test2.res test3.res
ima:
pushd ~/lurette/bin ; make -k dc -f Makefile.ima_exe OCAMLFLAGS=""; popd
......@@ -563,12 +574,17 @@ ima_nc:
show:
pushd ~/lurette/bin ; make -k dc -f Makefile.show_ima OCAMLFLAGS=""; popd
heater:
$(LURETTE_PATH)/make_lurette heater_int; \
heater_make:
$(LURETTE_PATH)/make_lurette heater_int
heater: heater_make
./lurette 30 1 1 temp_int.env --no-oracle
heaterf:
$(LURETTE_PATH)/make_lurette heater_float; \
heaterf_make:
$(LURETTE_PATH)/make_lurette heater_float
heaterf: heaterf_make
./lurette 30 1 1 temp_float.env --no-oracle
# In order to time profile lurette
......@@ -817,6 +833,9 @@ clean:
rm -f $(TARGETS) $(TRASH)
rm -rf $(BCDIDIR) $(NCDIDIR) $(MLDEPDIR)
sclean:
rm -f $(LURETTE_PATH)/source/lurette.cmx
.PHONY: cleanup
cleanup:
rm -f $(NONEXECS) $(TRASH)
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 72)
(Parent-Version lurette 0 71)
(Project-Version lurette 0 73)
(Parent-Version lurette 0 72)
(Version-Log "
sim2cro.ml:
switch inputs and output in the sim2chro display. The rational
is that local vars, are closer from ima outputs than sut ones.
and should then be displayed close to them.
gen_stubs.ml:
indent generated code better.
sim2chro.ml:
Do not sort varialble lexicographically but according to
sut order.
gen_stubs.ml:
When converting subst list to tuple, do not put fake values
if the list is empty, but raise a failure (assert false).
Do not parse idl output to guess the conversion between ml
and C type but hard code it instead. The rational is that
I was manually calling camlidl here which was confusing
make sometimes.
make_lurette:
exit properly before running lurette whenever something bad
happen during the make.
")
(New-Version-Log "")
(Checkin-Time "Tue, 23 Jul 2002 16:58:52 +0200")
(Checkin-Time "Mon, 29 Jul 2002 13:49:35 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -33,7 +44,7 @@ gen_stubs.ml:
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.42 644))
(source/lurette.ml (lurette/12_lurette.ml 1.43 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))
......@@ -45,7 +56,7 @@ gen_stubs.ml:
(source/env.mli (lurette/15_env.mli 1.15 644))
(source/env.ml (lurette/16_env.ml 1.29 644))
(source/util.ml (lurette/35_util.ml 1.22 644))
(source/util.ml (lurette/35_util.ml 1.23 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.25 644))
......@@ -74,20 +85,20 @@ gen_stubs.ml:
(source/automata.mli (lurette/b/46_automata.m 1.2 644))
(source/automata.ml (lurette/b/47_automata.m 1.2 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.9 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.10 644))
(source/gne.mli (lurette/b/36_gne.mli 1.2 644))
(source/gne.ml (lurette/b/37_gne.ml 1.2 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.27 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.28 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.14 744))
(make_lurette (lurette/27_make_luret 1.15 744))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.32 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.4 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.33 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.5 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.3 644))
......@@ -109,7 +120,7 @@ gen_stubs.ml:
(TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.1 644))
(test/time.res (lurette/b/49_time.res 1.3 644))
(test/time.res (lurette/b/49_time.res 1.4 644))
;; Various files used for testing purposes
(test/usager.env (lurette/b/14_usager.env 1.8 644))
......@@ -128,13 +139,13 @@ gen_stubs.ml:
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.5 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.6 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.7 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.4 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.1 644))
(test/test_gen_stubs.h (lurette/b/45_test_gen_s 1.1 644))
(test/Makefile (lurette/c/0_Makefile 1.1 644))
(test/Makefile (lurette/c/0_Makefile 1.2 644))
)
......
......@@ -37,9 +37,13 @@ case $# in
echo "... Generates the stub files (gen_stubs $1)"
$LURETTE_PATH/bin/gen_stubs $1
echo "... make"
shift 1
make $@
if test $? -eq 0; then
echo "... make"
shift 1
make $@
else
exit 1
fi
;;
##############################################################
*)
......@@ -52,9 +56,15 @@ case $# in
$LURETTE_PATH/bin/gen_stubs $1 $2
echo "... make"
shift 2
make $@
if test $? -eq 0; then
echo "... make"
shift 2
make $@
else
exit 1
fi
;;
esac
......
......@@ -9,6 +9,9 @@
**
*)
open List
(** Generates stub files for calling poc C programs from lurette. Its main
function takes as input the name of the sut and the name of the oracle
(file names without extension), and outputs all the necessary stub files.
......@@ -202,7 +205,7 @@ and
(** TEDLT! *)
let (replace_ct_by_their_alias: vn_ct list -> alias list -> vn_ct list) =
fun list alias ->
List.map (fun (vn, ct) -> (vn, (List.assoc ct alias))) list
List.rev_map (fun (vn, ct) -> (vn, (List.assoc ct alias))) list
let _ = assert ((replace_ct_by_their_alias [] []) = [])
let _ = assert (
......@@ -271,7 +274,7 @@ let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit)
let put s = output_string oc s in
let ov = List.rev vo in
let (lo_v, lo_t) = List.hd ov in
let vo_pre = List.tl ov in
let vo_pre = List.rev (List.tl ov) in
(*
** Compiler directive
......@@ -418,8 +421,65 @@ let (generate_idl : module_name -> sut_or_oracle -> vn_ct list -> vn_ct list
close_out oc
(****************************************************************************)
(****************************************************************************)
let (c_type_to_ml_type : string -> string) =
fun ct ->
(** I'm just following to the Camlidl doc here. *)
match ct with
"byte" -> "int"
| "short" -> "int"
| "short int" -> "int"
| "int" -> "int"
| "long" -> "int"
| "long int" -> "int"
| "unsigned short" -> "int"
| "unsigned short int" -> "int"
| "unsigned int" -> "int"
| "unsigned long" -> "int"
| "unsigned long int" -> "int"
| "char" -> "char"
| "unsigned char" -> "char"
| "float" -> "float"
| "double" -> "float"
| "long double" -> "float"
| "bool" -> "bool"
| "boolean" -> "bool"
| _ -> assert false
(** Translates C-poc type into lustre type *)
let c_type_to_lustre_type ct =
(* XXX That's pretty ugly... Fix me! *)
if
Util.is_substring "int" ct
then
"int"
else if
( (Util.is_substring "float" ct)
|| (Util.is_substring "real" ct)
|| (Util.is_substring "double" ct)
)
then
"real"
else if
Util.is_substring "bool" ct
then
"bool"
else
(
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
)
(****************************************************************************)
(**
[generate_n_var_names "x" 4] generates the list ["x1"; "x2"; "x3"; "x4"]
*)
......@@ -435,112 +495,6 @@ let _ = assert ((generate_n_var_names "x" 4) = ["x1"; "x2"; "x3"; "x4"])
(** cf get_ml_type *)
let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_ct_mlt_fvn list) =
fun file lin lout ->
let str = Util.readfile file in
let reg_external = Str.regexp "^external sut_step :" in
let reg_arrow = Str.regexp "->" in
let reg_eol = Str.regexp "\n" in
let rec (read_type_list: int -> string list -> string list) =
(*
** [read_type_list n []] returns the list of types (in reverse order)
** of the function sut_step, where n is the character position of the
** first char of the first type of sut_step.
*)
fun sptr acc ->
let (t, sptr1) = read_next_type sptr in
if (sptr1>0) then read_type_list sptr1 (t::acc)
else t::acc
and
(read_next_type: int -> string * int) =
fun sptr ->
let sptr1 = Str.search_forward reg_arrow str (sptr+1) in
let sptr2 = Str.search_forward reg_eol str (sptr+1) in
if (sptr1 < sptr2) then
(String.sub str (sptr+1) (sptr1 - sptr - 2), (sptr1+2))
else
(* last type *)
(String.sub str (sptr+1) (sptr2 - sptr - 1), -1)
in
let (sptr: int) =
(*
** [sptr] should point to the first char of the first
** type of sut_step.
*)
try
let sptr1 = Str.search_forward reg_external str 0 in
let sptr2 = Str.search_forward reg_blank str (sptr1+1) in
let sptr3 = Str.search_forward reg_blank str (sptr2+1) in
let sptr4 = Str.search_forward reg_blank str (sptr3+1) in
sptr4
with Not_found -> assert false
in
let (vtl: string list) = read_type_list sptr [] in
(*
** [vtl] ougth to contain the list of sut_try types in reverse order,
** i.e., the output type in the first place, then the last argument
** of (the currified version of) sut_try, and so on.
*)
let (sut_out_str, sut_in_list) =
match vtl with
sut_out_str::sut_in_list_rev ->
(sut_out_str, List.rev sut_in_list_rev)
(*
** Any ocaml function have at least one arrow, i.e.,
** vtl should contain at least 2 elements.
*)
| _ -> assert false
in
let sut_out_list = Str.split (Str.regexp " \\* ") sut_out_str in
(*
** Therefore now sut_out_str should be the type the sut_try output var,
** sut_in_str be the type of the sut input, and sut_in_list be the list
** of sut_try input vars (in the rigth order!).
*)
let (print_spl : (string * string) list -> unit) =
fun l ->
List.iter (fun (x,y) -> print_string ("(" ^ x ^ "," ^ y ^ ") ")) l
in
let (print_sl : string list -> unit) =
fun l ->
List.iter (fun x -> print_string (x ^ " ")) l
in
let _ =
if (List.length lin <> List.length sut_in_list)
then
(
output_string stderr "*** \t";
print_spl lin;
output_string stderr " does not have the same size as :\n\t";
print_sl sut_in_list;
output_string stderr "\n\n"
);
if (List.length lout <> List.length sut_out_list)
then
(
output_string stderr "*** \t";
print_spl lout;
output_string stderr " does not have the same size as :\n\t";
print_sl sut_out_list;
output_string stderr "\n\n"
);
in
(
(Util.list_map3
(fun (vn, ct) mlt fvn -> (vn, ct, mlt, fvn))
lin
sut_in_list
(generate_n_var_names "x" (List.length lin))),
(Util.list_map3
(fun (vn, ct) mlt fvn -> (vn, ct, mlt, fvn))
lout
sut_out_list
(generate_n_var_names "y" (List.length lout)))
)
(**
[get_ml_type sut_in sut_out] parses Sut_idl_stub.ml in order to get
the C-ocaml mapping used by camlidl. It returns 2 lists (the 1st one for
......@@ -550,7 +504,17 @@ let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_c
*)
let (get_ml_type: vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_ct_mlt_fvn list) =
fun lin lout ->
get_ml_type2 "sut_idl_stub.ml" lin lout
(
(map2
(fun (vn, ct) fvn -> (vn, ct, c_type_to_ml_type ct, fvn))
lin
(generate_n_var_names "x" (List.length lin))),
(map2
(fun (vn, ct) fvn -> (vn, ct, c_type_to_ml_type ct, fvn))
lout
(generate_n_var_names "y" (List.length lout)))
)
......@@ -602,17 +566,6 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
| "int" -> put (" \"" ^ vn ^ "\" -> Some(N(I(" ^ fvn ^ ")))")
| _ -> assert false
in
let (put_fake_value: vn_ct_mlt_fvn -> unit) =
(*
** Used to define sut_in_init ans sut_out_init.
*)
fun (_, _, mlt, _) ->
match mlt with
"bool" -> put "true"
| "float" -> put "0.0"
| "int" -> put "0"
| _ -> assert false
in
let vnl_in = List.map (fun (w,x,y,z) -> w) sut_in in
let vn_ctl_in = List.map (fun (w,x,y,z) -> (w,x)) sut_in in
let vn_mltl_in = List.map (fun (w,x,y,z) -> (w,y)) sut_in in
......@@ -694,19 +647,12 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
put "(** Converting tuples to subst lists and vive-versa *) \n\n";
put "let (subst_list_to_sut_in: subst list -> sut_in) =\n" ;
put " fun sl ->\n" ;
put " let sl_sorted = Util.sort_list_string_pair sl in\n";
put " match sl_sorted with\n" ;
put " match sl with\n" ;
put " [" ;
put (format_string_list "; \n\t " vn_val_in) ;
put "] \n\t -> (" ;
put (format_string_list ", \n\t " fvnl_in) ;
put ")\n";
put " | [] -> (" ;
put_fake_value (List.hd sut_in) ;
List.iter
(fun x -> put ", "; put_fake_value x)
(List.tl sut_in) ;
put ")\n";
put " | _ -> assert false\n\n" ;
......@@ -894,22 +840,27 @@ let main2 sut oracle =
let oracle_vo = replace_ct_by_their_alias oracle_vo0 oracle_alias in
(*
** Sorts variables lexicographically w.r.t. to their names.
*)
let (sort_vars: vn_ct list -> vn_ct list) =
fun var_list ->
List.sort (fun (vn1, t1) (vn2, t2) -> compare vn1 vn2) var_list
** Sorts variables w.r.t. to their order in the sut.
*)
let (sort_vars: string list -> vn_ct list -> vn_ct list) =
fun ref_list var_list ->
List.sort
(fun (vn1, t1) (vn2, t2) -> Util.compare_list ref_list vn1 vn2)
var_list
in
let sut_vi_ord = sut_vi in
let sut_vo_ord = sut_vo in
let vi_list_ref = fst (split sut_vi)
and vo_list_ref = fst (split sut_vo)
in
let sut_vi_ord = sort_vars sut_vi in
let sut_vo_ord = sort_vars sut_vo in
let oracle_vi_ord = List.append sut_vi_ord sut_vo_ord in
let oracle_vi_ord_decl = sort_vars oracle_vi in
let sut_vars_ord = sort_vars (List.append sut_vi sut_vo) in
let v_list_ref = append vi_list_ref vo_list_ref in
let oracle_vi_ord = List.append sut_vi sut_vo in
let oracle_vi_ord_decl = sort_vars v_list_ref oracle_vi in
(*
** Aborts if the variables are inconsistent in the sut and in the oracle.
*)
(match check_var_type sut_vars_ord oracle_vi_ord_decl oracle_vo with
(match check_var_type oracle_vi_ord oracle_vi_ord_decl oracle_vo with
Ok -> () | Error(err_msg) -> failwith err_msg );
generate_stub_c sut_m "sut" sut_vi_ord sut_vo_ord ;
......@@ -918,6 +869,8 @@ let main2 sut oracle =
generate_stub_c oracle_m "oracle" oracle_vi_ord oracle_vo ;
generate_idl oracle_m "oracle" oracle_vi_ord oracle_vo ;
generate_lurette_stub_file (get_ml_type sut_vi_ord sut_vo_ord) ;
(* Update the stubs iff they have changed to avoid unnecessary re-compilations *)
update_file "sut_idl_stub.idl.new" "sut_idl_stub.idl" ;
update_file "sut_stub.c.new" "sut_stub.c" ;
......@@ -925,44 +878,14 @@ let main2 sut oracle =
update_file "oracle_idl_stub.idl.new" "oracle_idl_stub.idl" ;
update_file "oracle_stub.c.new" "oracle_stub.c" ;
(* We need to call camlidl now in order to get the ocaml types of the sut. *)
if
not (Sys.file_exists "sut_idl_stub.idl.new")
(* iff sut_idl_stub.ml has changed *)
then
if ((Sys.command ("echo \"... camlidl -header sut_idl_stub.idl \" ;"
^ " camlidl -header sut_idl_stub.idl "))