Commit 74f93d6c authored by Erwan Jahier's avatar Erwan Jahier

Add ocaml support in lurette.

For the time being, it crashes if no valid oracle.ml exists in the
user directory. Moreover, and the sut has to be named 'sut.ml' (resp.
oracle.ml for the oracle). But otherwise, it works fine.
parent 10b66fa4
......@@ -40,7 +40,7 @@ ci: test
diff:
git diff HEAD -w > diff.diff && \
git diff HEAD -w > diff.diff
echo "il y a $(shell grep "+" diff.diff | wc -l) + et $(shell grep "-" diff.diff | wc -l) -"
......
......@@ -15,6 +15,7 @@ test:
cd lucky/C && make test ;
cd lucky/lustre && make test ;
cd lucky/luciole && make test ;
cd ocaml/xlurette && make test ;
ifneq ($(HOST_TYPE),mac)
# cd xlurette/Sildex/ && make test ;
cd ocaml/crazy-rabbit/ && make test ;
......
LTOP=../../../$(HOST_TYPE)/bin/lurettetop
LURETTETOP=$(LTOP) --precision 2 --sut sut.ml \
--sut-compiler ocaml \
--oracle-compiler ocaml --oracle oracle.ml \
--test-length 500 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step
# XXX
# --oracle oracle.ml \
test:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) -go --output test.rif0 sensors.luc && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
utest:
cp test.rif test.rif.exp
clean:
rm -rf *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp
test_dontgo:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) --output test.rif0 sensors.luc && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
(* Time-stamp: <modified the 13/07/2010 (at 15:49) by Erwan Jahier> *)
let init _ = ()
type str_type = string
(* An str_type can be "bool", "int", or "float" *)
let (get_input_var_name_and_type : unit -> (string * str_type) list) =
fun () -> ["T", "float"; "T1", "float"; "T2", "float"; "T3", "float";"Heat_on", "bool"]
let (get_output_var_name_and_type : unit -> (string * str_type) list) =
fun () -> ["ok", "bool"]
open Value
let (step : (string * Value.t) list -> (string, Value.t) Hashtbl.t -> bool* Var.subst list) =
fun inputs outputs ->
let t =
try
List.assoc "T" inputs
with Not_found ->
print_string ("oracle.ml: can not find variable T in the list of sut inputs\n");
print_string ("Available variables are: " ^ (String.concat ", " (fst (List.split inputs))));
print_string ("\n");
flush stdout;
exit 2
in
let ok =
match t with
N(F(f)) -> f < 10.0
| _ -> assert false
in
ok, ["ok", (B(ok))]
(* Trie save the current state of the SUT, perfoms a step, and restore the saved state
nb : i cannot call it try, it is an ocaml kwd ... *)
let (trie : (string * Value.t) list -> (string, Value.t) Hashtbl.t -> bool* Var.subst list)=
fun inputs outputs ->
step inputs outputs
-- Simulate perfect sensors that never get worn
inputs { Heat_on : bool }
outputs {
T : float ~min 0.0 ~max 50.0;
T1 : real;
T2 : real;
T3 : real
}
locals {
eps1 : real ~min -0.1 ~max 0.1;
eps2 : real ~min -0.1 ~max 0.1;
eps3 : real ~min -0.1 ~max 0.1;
}
nodes { 0,1 : stable }
start_node { 0 }
transitions {
0 -> 1 ~cond T = 7.0
and T1 = T + eps1
and T2 = T + eps2
and T3 = T + eps3
;
1 -> 1 ~ cond T = pre T + (if Heat_on then 0.2 else -0.2)
and T1 = T + eps1
and T2 = T + eps2
and T3 = T + eps3
}
(* Time-stamp: <modified the 13/07/2010 (at 15:47) by Erwan Jahier> *)
let init _ = ()
let pre_res = ref false
type str_type = string
(* An str_type can be "bool", "int", or "float" *)
let (get_input_var_name_and_type : unit -> (string * str_type) list) =
fun () -> ["T", "float"; "T1", "float"; "T2", "float"; "T3", "float"]
let (get_output_var_name_and_type : unit -> (string * str_type) list) =
fun () -> ["Heat_on", "bool"]
let tbl = Hashtbl.create 0
open Value
let (step : (string * Value.t) list -> (string, Value.t) Hashtbl.t) =
fun inputs ->
let t = List.assoc "T" inputs in
let res =
match t with
N(F(f)) -> if f > 9.0 then false else if f < 6.00 then true else !pre_res
| _ -> assert false
in
pre_res := res;
Hashtbl.replace tbl "Heat_on" (B(res));
tbl
(* Trie save the current state of the SUT, perfoms a step, and restore the saved state
nb : i cannot call it try, it is an ocaml kwd ... *)
let (trie : (string * Value.t) list -> (string, Value.t) Hashtbl.t)=
fun l ->
step l
(** Where module Value is defined as follows:
type num = I of int | F of float
type t = B of bool | N of num
*)
This diff is collapsed.
......@@ -12,7 +12,7 @@ endif
test1:
$(RM) test1.rif0 && \
$(LURETTETOP) \
-l 30 -td 10 --sut heater_ctrl_int -msn heater_ctrl_int --seed 1 \
-l 30 -td 10 --sut heater_ctrl_int.lus -msn heater_ctrl_int --seed 1 \
--draw-inside 10 --draw-edges 10 --draw-all-vertices --draw-vertices 10 \
--do-not-show-step -ns2c -go -o test1.rif0 --draw-inside 10 --draw-edges 10 \
-go temp_int.luc &&\
......
......@@ -81,6 +81,34 @@ lurette.dro: lurette_luciole.o
all: nc
##############################################################################
#
# Ocaml
sut.ml:
cp $(USER_TESTING_DIR)/sut.ml .
sut.mli:
cp $(LURETTE_PATH)/lib/sut.mli .
oracle.ml:
cp $(USER_TESTING_DIR)/oracle.ml .
oracle.mli:
cp $(LURETTE_PATH)/lib/oracle.mli .
SOURCES_ML = oracle.mli oracle.ml sut.mli sut.ml $(EXTRA_ML_FILES)
ocaml: sut.ml sut.mli oracle.ml oracle.mli
ocamlopt.opt \
-I $(LURETTE_PATH)/lib \
-ccopt -L $(LURETTE_PATH)/lib \
str.cmxa unix.cmxa nums.cmxa polka.cmxa bdd.cmxa \
$(SOURCES_ML) lurette_ml_exec.cmxa $(LURETTE_PATH)/lib/lurette_exec.ml \
-o lurette
##############################################################################
#
......
......@@ -52,7 +52,7 @@ let lurette_bin = (Filename.concat lurette_path "bin")
(* compiler used to compiler sut and oracles *)
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex | Stdin
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex | Stdin | Ocaml
type step_mode = | Inside | Edges | Vertices
let string_to_step_mode = function
......@@ -259,6 +259,7 @@ let (string_to_compiler:string -> compiler option) =
| "stdin/stdout" -> Some Stdin
| "stdin" -> Some Stdin
| "Stdin" -> Some Stdin
| "ocaml" -> Some Ocaml
| _ -> None
let (compiler_to_string : compiler -> string) =
......@@ -270,6 +271,7 @@ let (compiler_to_string : compiler -> string) =
| ScadeGUI -> "scade-gui"
| Sildex -> "sildex"
| Stdin -> "stdin"
| Ocaml -> "ocaml"
let (compiler_to_extension : compiler -> string) =
fun c ->
......@@ -280,18 +282,7 @@ let (compiler_to_extension : compiler -> string) =
| ScadeGUI -> assert false (* we should not need to compile any thing in that mode *)
| Sildex -> assert false (* XXX what is the extension of sildex files? *)
| Stdin -> assert false
let (add_a_default_extension_if_needed : string -> string) =
fun file ->
(* Add a .lus extension if none is provided *)
try
let _ = Filename.chop_extension file in
file
with
Invalid_argument _ ->
output_string !ecr ("No extension is provided for " ^ file ^
". We assume it is a .lus\n");
(file ^ ".lus")
| Ocaml -> ".ml"
(* XXX windows *)
......@@ -363,10 +354,10 @@ let _ = assert ((remove_extension "home/toto/tutu") = "home/toto/tutu")
let rec speclist =
[
"--sut", Arg.String
(fun file -> flag.sut <- add_a_default_extension_if_needed file),
(fun file -> flag.sut <- file),
"<string>\tFile name of the system under test.";
"-sut", Arg.String
(fun file -> flag.sut <- add_a_default_extension_if_needed file),
(fun file -> flag.sut <- file),
" <string>\n" ;
"--sut-cmd", Arg.String
......@@ -391,10 +382,10 @@ let rec speclist =
" <string>\n" ;
"--oracle", Arg.String (fun file -> flag.oracle <-
Some (add_a_default_extension_if_needed file)),
Some (file)),
"<string>\tFile name of the oracle.";
"-oracle", Arg.String (fun file -> flag.oracle <-
Some (add_a_default_extension_if_needed file)),
Some (file)),
" <string>\n";
"--main-oracle-node", Arg.String
......@@ -798,6 +789,8 @@ let (build : string -> bool) =
| VerimagV6, VerimagV4 -> make_rule
| VerimagV6, VerimagV6 -> make_rule
| VerimagV4, VerimagV4 -> make_rule
| Ocaml, _ -> "ocaml"
| _, Ocaml -> "ocaml"
| Sildex, VerimagV4 -> "sildex_sut"
| VerimagV4, Sildex -> "sildex_oracle"
| Sildex, Sildex -> "sildex_both"
......@@ -838,19 +831,30 @@ let (build : string -> bool) =
try
Unix.chdir flag.tmp_dir;
Unix.putenv "SUT_DIR" flag.tmp_dir;
Unix.putenv "SUT" sut_node;
if flag.sut_compiler = Ocaml then
Unix.putenv "SUT" flag.sut
else
Unix.putenv "SUT" sut_node;
Unix.putenv "ENV" flag.env;
(match flag.pp with None -> () |
Some pp -> Unix.putenv "PP" ("-pp "^ (pp)));
Unix.putenv "ORACLE_DIR" oracle_dir;
Unix.putenv "ORACLE" oracle_node;
if flag.oracle_compiler = Ocaml then
(match flag.oracle with
None-> ()
| Some str -> Unix.putenv "ORACLE" str)
else
Unix.putenv "ORACLE" oracle_node;
Unix.putenv "USER_TESTING_DIR" (flag.sut_dir);
Unix.putenv "LURETTE_TMP_DIR" (flag.tmp_dir);
if
not (gen_stubs (Filename.concat flag.sut_dir flag.sut) sut_node
(if oracle = "" then "" else oracle)
(if oracle = "" then "" else oracle_node)
)
if flag.sut_compiler <> Ocaml then (
not (gen_stubs (Filename.concat flag.sut_dir flag.sut) sut_node
(if oracle = "" then "" else oracle)
(if oracle = "" then "" else oracle_node)
))
else false
then
false
else
......@@ -1594,6 +1598,7 @@ set_sut_compiler <string>
| ScadeGUI -> "\"scade-gui\""
| Sildex -> "\"sildex\""
| Stdin -> "\"stdin\""
| Ocaml -> "\"ocaml\""
) ^ "
set_oracle_compiler <string>
......@@ -1605,6 +1610,7 @@ set_oracle_compiler <string>
| ScadeGUI -> "\"scade-gui\""
| Sildex -> "\"sildex\""
| Stdin -> "\"stdin\""
| Ocaml -> "\"ocaml\""
) ^ "
......@@ -2770,6 +2776,7 @@ let main_read_arg () =
| ScadeGUI -> true
| Sildex -> true
| Stdin -> true
| Ocaml -> true
| Scade ->
Util2.cp (Filename.concat source_dir "memories.c") flag.tmp_dir !ocr !ecr
&&
......
......@@ -3,7 +3,6 @@
-include ../Makefile.common.source
-include ./Makefile.ln
OBJDIR=./obj-$(HOSTTYPE)
## to override those, do 'export COMPIL_MODE=bc && make blablabla'
......@@ -24,7 +23,8 @@ LIB_INSTALL_DIR = ../$(HOST_TYPE)/lib
INC_INSTALL_DIR = ../$(HOST_TYPE)/include
$(OBJDIR) :
OBJDIR=./obj-$(HOSTTYPE)
$(OBJDIR):
mkdir $(OBJDIR)
......@@ -32,8 +32,8 @@ $(OBJDIR) :
# destin a etre appelle depuis ocaml uniquement.
liblucky_nc.a: liblutin_stubs.o $(OBJDIR)
cd $(OBJDIR) && \
[ -d lurette_util ] || mkdir lurette_util && \
cd lurette_util && rm -f * && \
[ -d lurette_tmp ] || mkdir lurette_tmp && \
cd lurette_tmp && rm -f * && \
ar rcs liblucky_nc.a \
../../$(OBJDIR)/liblutin_stubs.o ../../$(OBJDIR)/liblutin_c.o \
../../$(OBJDIR)/Ezdl_c.o &&\
......@@ -62,8 +62,8 @@ liblutin_stubs.o:$(OBJDIR)
.PHONY:liblucky_nc.so liblutin_stubs.o
liblucky_nc.so: liblutin_stubs.o $(OBJDIR)
cd $(OBJDIR) && \
[ -d lurette_util ] || mkdir lurette_util && \
cd lurette_util && rm -f * && \
[ -d lurette_tmp ] || mkdir lurette_tmp && \
cd lurette_tmp && rm -f * && \
cp ../Ezdl_c.o . &&\
cp ../liblutin_stubs.o . &&\
cp ../liblutin_c.o . &&\
......@@ -83,27 +83,28 @@ ocaml2c_stubs.o: lurette_lib.o$(EXE)
lurette_exe.o:lurette_lib.o$(EXE)
call_lurette_main.o:lurette_lib.o$(EXE)
lib$(COMPIL_MODE):liblurette_$(COMPIL_MODE).a
lib$(COMPIL_MODE): liblurette_$(COMPIL_MODE).a
# On rajoute asmrun + les fichiers spcifiques lurette.
liblurette_$(COMPIL_MODE).a: ocaml2c_stubs.o lurette_exe.o call_lurette_main.o lurette_lib.o$(EXE) liblucky_nc.a $(OBJDIR)
liblurette_$(COMPIL_MODE).a: lurette_exe.o call_lurette_main.o lurette_lib.o$(EXE) liblucky_nc.a $(OBJDIR)
cd $(OBJDIR) &&\
[ -d lurette_util ] || mkdir lurette_util && \
cd lurette_util && rm -f * && \
[ -d lurette_tmp ] || mkdir lurette_tmp && \
cd lurette_tmp && rm -f * && \
ar rcs liblurette_nc.a ../lurette_lib.o$(EXE) \
../ocaml2c_stubs.o ../lurette_exe.o ../call_lurette_main.o && \
../ocaml2c_stubs.o ../lurette_exe.o ../call_lurette_main.o && \
ar x $(OCAMLLIB)/libasmrun.a &&\
ar q liblurette_$(COMPIL_MODE).a *.o && rm *.o &&\
cp liblurette_$(COMPIL_MODE).a ..
luc4c_lib.o: luc4c_lib.o
luc4c_stubs.o:luc4c_lib.o
libluc4c_$(COMPIL_MODE).a: luc4c_lib.o luc4c_stubs.o Lucky/luc4c.ml $(OBJDIR)
cd $(OBJDIR) && \
[ -d lurette_util ] || mkdir lurette_util && \
cd lurette_util && rm -f * && \
[ -d lurette_tmp ] || mkdir lurette_tmp && \
cd lurette_tmp && rm -f * && \
ar rcs libluc4c_$(COMPIL_MODE).a ../luc4c_lib.o \
../luc4c_stubs.o && \
ar x $(OCAMLLIB)/libasmrun.a &&\
......@@ -114,8 +115,8 @@ libluc4c_$(COMPIL_MODE).a: luc4c_lib.o luc4c_stubs.o Lucky/luc4c.ml $(OBJDIR)
.PHONY:libluc4c_nc.so
libluc4c_nc.so: Lucky/luc4c_lib.o Lucky/luc4c_stubs.o Lucky/luc4c.ml $(OBJDIR)
cd $(OBJDIR) &&\
[ -d lurette_util ] || mkdir lurette_util && \
cd lurette_util && rm -f * && \
[ -d lurette_tmp ] || mkdir lurette_tmp && \
cd lurette_tmp && rm -f * && \
cp ../luc4c_lib.o . && \
cp ../luc4c_stubs.o . && \
ar x $(OCAMLLIB)/libasmrun.a &&\
......@@ -131,7 +132,7 @@ libluc4c_nc.so_bis: $(OBJDIR)
common/lurette_lib.o$(EXE): libncnc
liblurette_bc.a: $(OBJDIR)/lurette_lib.o$(EXE) $(OBJDIR)
cd $(OBJDIR)/lurette_util && rm -f * &&\
cd $(OBJDIR)/lurette_tmp && rm -f * &&\
ar rcs liblurette_bc.a ../lurette_lib.o$(EXE) &&\
ar x $(HOME)/$(HOST_TYPE)/lib/libcudd_caml.a &&\
ar r liblurette_bc.a *.o && rm *.o &&\
......@@ -162,7 +163,7 @@ liblurette_bc.a: $(OBJDIR)/lurette_lib.o$(EXE) $(OBJDIR)
cp liblurette_bc.a ..
liblurette_dc.a:
cd lurette_util &&rm * &&\
cd lurette_tmp &&rm * &&\
ar rcs liblurette_dc.a ../lurette_lib.o$(EXE) &&\
ar x $(HOME)/$(HOST_TYPE)/lib/bdd.a &&\
ar r liblurette_dc.a *.o && rm *.o &&\
......@@ -191,7 +192,7 @@ liblurette_dc.a:
cp liblurette_dc.a ..
liblurette_pbc.a:
cd lurette_util &&rm * &&\
cd lurette_tmp &&rm * &&\
ar rcs liblurette_pbc.a ../lurette_lib.o$(EXE) &&\
ar x $(HOME)/$(HOST_TYPE)/lib/libcudd_caml.a &&\
ar r liblurette_pbc.a *.o && rm *.o &&\
......@@ -234,19 +235,10 @@ lurette_lib.o: $(OBJDIR)
make $(COMPIL_MODE) -f ../common/Makefile.lurette_lib
liblurette_gprof.a: clean $(OBJDIR)
export COMPIL_MODE=pncl && cd $(OBJDIR) && \
make pncl -f ../common/Makefile.lurette_lib OCAMLFLAGS="" &&\
cp `ocamlc -where`/libcamlrun.a liblurette_gprof.a && \
ar r liblurette_gprof.a lurette_lib.o
liblurette_prof.a:
export COMPIL_MODE=pncl && cd $(OBJDIR) && \
make pbcl -f ../common/Makefile.lurette_lib OCAMLFLAGS="" &&\
cp `ocamlc -where`/libcamlrun.a liblurette_prof.a && \
ar r liblurette_prof.a lurette_lib.o
lurette_ml_exec: $(OBJDIR)
cd $(OBJDIR) && \
make ln -f ../common/Makefile.lurette4ocaml && \
make $(COMPIL_MODE)l -f ../common/Makefile.lurette4ocaml
-include ./Makefile.release
......@@ -334,9 +326,9 @@ draw-install:
cp -f libluckyDraw*.a $(CAML_INSTALL_DIR)/lucky
draw-cp: luckyDraw.top libluckyDraw.a
cp common/luckyDraw.top ../$(HOST_TYPE)/bin || true
cp -f common/luckyDraw.* ../$(HOST_TYPE)/lib
cp -f common/libluckyDraw*.a ../$(HOST_TYPE)/lib
cp $(OBJDIR)/luckyDraw.top ../$(HOST_TYPE)/bin || true
cp -f $(OBJDIR)/luckyDraw.* ../$(HOST_TYPE)/lib
cp -f $(OBJDIR)/libluckyDraw*.a ../$(HOST_TYPE)/lib
ranlib ../$(HOST_TYPE)/lib/*.a
draw-source-pack:
......@@ -537,9 +529,9 @@ all_assert:
check:
echo "A faire dans le repertoire test, sinon, ca vaut pas !!! "
allw: clean lucky libncltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c_$(COMPIL_MODE).a draw-all luc4ocaml-all
all: lucky libnc ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c_$(COMPIL_MODE).a draw-all luc4ocaml-all
allnc: clean lucky libncnc ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c_$(COMPIL_MODE).a draw-all luc4ocaml-all
allw: clean lurette_ml_exec lucky libncltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c_$(COMPIL_MODE).a draw-all luc4ocaml-all
all: clean $(OBJDIR) lurette_ml_exec lucky libnc ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c_$(COMPIL_MODE).a draw-all luc4ocaml-all
allnc: clean lurette_ml_exec lucky libncnc ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc2luciole luc4c libluc4c_$(COMPIL_MODE).a draw-all luc4ocaml-all
static: libnc lucky_static ltop_static show_static stubs_static gen_luc_static
......@@ -564,7 +556,7 @@ clean_exe:
liblurette_lib*
clean: $(OBJDIR)
rm -rf $(OBJDIR)
rm -rf $(OBJDIR)/*
cp:
......@@ -584,6 +576,11 @@ cp:
cp $(OBJDIR)/liblurette_nc.a $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/liblucky_nc.a $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/libluc4c_nc.a $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/*lurette_ml_exec*a $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/*.cmi $(LIB_INSTALL_DIR) ;\
cp common/lurette_exec.ml $(LIB_INSTALL_DIR) ;\
cp common/sut.mli $(LIB_INSTALL_DIR) ;\
cp common/oracle.mli $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/ocaml2c.h $(INC_INSTALL_DIR) ;\
cp $(OBJDIR)/droconf.h $(INC_INSTALL_DIR) ;\
cp $(OBJDIR)/luc4c_stubs.h $(INC_INSTALL_DIR) ;\
......@@ -606,6 +603,11 @@ cp-verimag:
cp Lurettetop/lurettetop_exe$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp common/liblurette_nc.a $(LIB_VERIMAG_INSTALL_DIR) ;\
cp common/liblucky_nc.a $(LIB_VERIMAG_INSTALL_DIR) ;\
cp $(OBJDIR)/*lurette_ml_exec*a $(LIB_VERIMAG_INSTALL_DIR) ;\
cp $(OBJDIR)/*.cmi $(LIB_VERIMAG_INSTALL_DIR) ;\
cp common/lurette_exec.ml $(LIB_VERIMAG_INSTALL_DIR) ;\
cp common/sut.mli $(LIB_VERIMAG_INSTALL_DIR) ;\
cp common/oracle.mli $(LIB_VERIMAG_INSTALL_DIR) ;\
cp common/libluc4c_nc.a $(LIB_VERIMAG_INSTALL_DIR) ;\
cp common/ocaml2c.h $(INC_VERIMAG_INSTALL_DIR) ;\
cp Lucky/luc4c_stubs.h $(INC_VERIMAG_INSTALL_DIR) ;\
......
......@@ -275,6 +275,11 @@ luc4ocaml-rel:
cp ../$(HOSTTYPE)/lib/libgmp.a /tmp/$(LUC4OCAML_RELEASE_NAME)/lib || true
cp ../$(HOSTTYPE)/lib/*luc4ocaml*.* /tmp/$(LUC4OCAML_RELEASE_NAME)/lib
\
cp ../$(HOSTTYPE)/lib/*lurette_ml_exec*a /tmp/$(LUC4OCAML_RELEASE_NAME)/lib ;\
cp ../$(HOSTTYPE)/lib/lurette_exec.ml /tmp/$(LUC4OCAML_RELEASE_NAME)/lib ;\
cp ../$(HOSTTYPE)/lib/sut.mli /tmp/$(LUC4OCAML_RELEASE_NAME)/lib ;\
cp ../$(HOSTTYPE)/lib/oracle.mli /tmp/$(LUC4OCAML_RELEASE_NAME)/lib ;\
\
cp -rf $(LURETTE_PATH)/$(HOSTTYPE)/lib/*polka*a /tmp/$(LUC4OCAML_RELEASE_NAME)/lib
cp -rf $(LURETTE_PATH)/$(HOSTTYPE)/lib/*bdd*a /tmp/$(LUC4OCAML_RELEASE_NAME)/lib
cp $(CAML_INSTALL_DIR)/libcamlidl.a /tmp/$(LUC4OCAML_RELEASE_NAME)/lib
......
#
# Makefile for lurette
#
-include ../../Makefile.common.source
-include ../Makefile.ln
######################################################################
OCAMLNCFLAGS = -inline 10
ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
endif
OCAMLFLAGS += -I ../$(OBJDIR) -I $(OCAMLLIB) -I $(PREFIX)/$(HOSTTYPE)/lib
CC=gcc -O2 $(DWIN32)
DEBUG=
ifeq ($(HOST_TYPE),win32)
IDLFLAGS=-nocpp
endif
ifeq ($(HOST_TYPE),mac)
IDLFLAGS=-nocpp
endif
POLKA=polkag
OCAMLLDFLAGS = -cclib -lstdc++ -cclib -lm -cclib -lc \
-cclib -l$(POLKA)_caml -cclib -l$(POLKA) -cclib -lgmp $(OCAMLOPTFLAG) -cclib -lcamlidl
# -verbose -cclib -lcudd_caml$(DEBUG) -cclib -lcuddaux$(DEBUG) -cclib -lcudd \
LIBS = str unix nums polka bdd
# POLKA_CLIB = polkag_caml polkag gmp
# CLIBS = cudd_caml cuddaux cudd $(POLKA_CLIB) camlidl mtr st epd util