Skip to content

GitLab

Commit 03ffa20e authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.58 Fri, 19 Apr 2002 11:15:07 +0200 by jahier 

Parent-Version:      0.57
Version-Log:

Clean up Makefiles for lurette and ima_exe.

Make sure that gen_stubs does not recompile the fake oracle
(always_true.lus) if it is not necessary.

Project-Description: Lurette
parent da601f66
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ 03ffa20e
......@@ -9,35 +9,35 @@
(source/util.ml 11635 1017837703 35_util.ml 1.17)
(source/wtree.ml 8518 1016011748 b/1_wtree.ml 1.9)
(source/solver.ml 24560 1017837703 39_solver.ml 1.21)
(source/command_line.ml 4234 1017396284 b/20_command_li 1.5)
(source/lurette.ml 11389 1017837703 12_lurette.ml 1.33)
(source/command_line.ml 4388 1019207707 b/20_command_li 1.7)
(source/lurette.ml 11547 1017929190 12_lurette.ml 1.34)
(source/solver.mli 1135 1016803757 38_solver.mli 1.10)
(source/env.mli 2593 1017396284 15_env.mli 1.11)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 10895 1017750312 16_env.ml 1.23)
(make_lurette 1149 1017335442 27_make_luret 1.8)
(make_lurette 1250 1019207707 27_make_luret 1.10)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 952 1017843266 b/17_passerelle 1.5)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 10783 1017837703 b/27_rnumsolver 1.6)
(source/parse_env.mli 907 1016127950 40_parse_env. 1.6)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
(source/parse_env.mli 907 1016127950 40_parse_env. 1.6)
(source/sim2chro.mli 1429 1017929190 b/23_sim2chro.m 1.4)
(source/ima_exe.ml 7206 1017750312 b/32_ima_exe.ml 1.4)
(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 35425 1017335442 24_generate_l 1.21)
(source/gen_stubs.ml 35799 1019207707 24_generate_l 1.22)
(source/parse_env.ml 16928 1017843266 41_parse_env. 1.15)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2663 1016803757 b/24_sim2chro.m 1.6)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/sim2chro.ml 2680 1017929190 b/24_sim2chro.m 1.7)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 3402 1017837703 44_formula.ml 1.10)
(TAGS 9825 1007379917 21_TAGS 1.6)
(test/Makefile_ima_exe 1625 1017750312 b/35_Makefile_i 1.3)
(source/command_line.mli 1384 1017396284 b/21_command_li 1.5)
(test/Makefile_ima_exe 163 1019207707 b/35_Makefile_i 1.4)
(source/command_line.mli 1421 1017929190 b/21_command_li 1.6)
(source/wtree.mli 2340 1016011748 b/0_wtree.mli 1.7)
(test/porte.env 977 1017843266 b/16_porte.env 1.5)
(source/env_state.mli 5168 1017750312 50_env_state. 1.15)
......@@ -46,19 +46,21 @@
(source/eval.mli 1389 1016803757 48_eval.mli 1.9)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 19265 1017396284 17_OcamlMakef 1.25)
(OcamlMakefile 19151 1019207707 17_OcamlMakef 1.26)
(source/command_line_ima_exe.ml 2400 1016803757 b/33_command_li 1.2)
(test/ControleurPorte.rif.exp 4746 1016803757 b/29_Controleur 1.4)
(test/tram.env 1019 1017843266 b/15_tram.env 1.5)
(Makefile.lurette 1848 1019207707 b/38_Makefile.l 1.1)
(source/show_env.ml 2971 1017750312 43_show_env.m 1.4)
(source/gne.mli 1107 1016803757 b/36_gne.mli 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(Makefile.ima_exe 1658 1019207707 b/39_Makefile.i 1.1)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(interface/Makefile 221 1019207707 25_Makefile 1.7)
(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
(test/Makefile 164 1019207707 18_Makefile 1.29)
(source/gne.ml 8204 1016803757 b/37_gne.ml 1.1)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1835 1017837703 18_Makefile 1.27)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 789 1016803757 46_print.mli 1.8)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
......
Makefile deleted 100644 → 0
View file @ da601f66
LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
# OCAMLFLAGS = -noassert -unsafe
OCAMLNCFLAGS = -inline 10
-include ./lurette.in
INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib
# Requires cudd and mldd to be installed!
LIBS = str nums # mlpoly
CLIBS = cudd_caml cuddaux cudd mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes
SOURCES_C = $(SUT) sut_stub.c sut_idl_stub.idl \
$(ORACLE) oracle_stub.c oracle_idl_stub.idl
# $(LURETTE_DIR)/source/pnumsolver.mli $(LURETTE_DIR)/source/pnumsolver.ml
SOURCES_OCAML = \
$(LURETTE_DIR)/source/util.ml \
$(LURETTE_DIR)/source/graph.mli $(LURETTE_DIR)/source/graph.ml \
$(LURETTE_DIR)/source/command_line.mli $(LURETTE_DIR)/source/command_line.ml \
$(LURETTE_DIR)/source/formula.mli $(LURETTE_DIR)/source/formula.ml \
$(LURETTE_DIR)/source/gne.mli $(LURETTE_DIR)/source/gne.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/rnumsolver.mli $(LURETTE_DIR)/source/rnumsolver.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
$(LURETTE_DIR)/source/sim2chro.mli $(LURETTE_DIR)/source/sim2chro.ml \
$(LURETTE_DIR)/source/env.mli $(LURETTE_DIR)/source/env.ml \
lurette_stub.ml \
$(LURETTE_DIR)/source/lurette.mli $(LURETTE_DIR)/source/lurette.ml
SOURCES = $(SOURCES_C) \
$(SOURCES_OCAML)
RESULT = lurette
-include $(OCAMLMAKEFILE)
Makefile.ima_exe 0 → 100644
View file @ 03ffa20e
#
# Makefile for ima_exe based on OcamlMakefile
#
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
OCAMLNCFLAGS = -inline 10
ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
endif
# Requires cudd and mldd to be installed!
LIBS = str nums # mlpoly
CLIBS = cudd_caml cuddaux cudd camlidl mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes
SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line_ima_exe.mli $(LURETTE_PATH)/source/command_line_ima_exe.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
$(LURETTE_PATH)/source/ima_exe.mli $(LURETTE_PATH)/source/ima_exe.ml
SOURCES = $(SOURCES_C) \
$(SOURCES_OCAML)
RESULT = ima_exe
-include $(OCAMLMAKEFILE)
Makefile.lurette 0 → 100644
View file @ 03ffa20e
#
# Makefile for lurette based on OcamlMakefile
#
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
OCAMLNCFLAGS = -inline 10
ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
endif
# Requires cudd and mldd to be installed!
LIBS = str nums # mlpoly
CLIBS = cudd_caml cuddaux cudd mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes
SOURCES_C = $(SUT) sut_stub.c sut_idl_stub.idl \
$(ORACLE) oracle_stub.c oracle_idl_stub.idl
# $(LURETTE_PATH)/source/pnumsolver.mli $(LURETTE_PATH)/source/pnumsolver.ml
SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/wtree.mli $(LURETTE_PATH)/source/wtree.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
lurette_stub.ml \
$(LURETTE_PATH)/source/lurette.mli $(LURETTE_PATH)/source/lurette.ml
SOURCES = $(SOURCES_C) \
$(SOURCES_OCAML)
RESULT = lurette
-include $(OCAMLMAKEFILE)
OcamlMakefile
View file @ 03ffa20e
......@@ -5,10 +5,9 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.25 Fri, 29 Mar 2002 11:04:44 +0100 jahier $
# $Id: OcamlMakefile 1.26 Fri, 19 Apr 2002 11:15:07 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
# the result variable. Order matters during linkage!
......@@ -383,7 +382,15 @@ endif
###########################################################################
# generates byte-code (default)
# generates native-code (default)
native-code: $(PRE_TARGETS)
@$(MAKE) -r -f $(OCAMLMAKEFILE) $(NCRESULT) \
REAL_RESULT="$(NCRESULT)" \
REAL_OCAMLC="$(OCAMLOPT)" \
make_deps=yes
nc: native-code
# generates byte-code
byte-code: $(PRE_TARGETS)
@$(MAKE) -r -f $(OCAMLMAKEFILE) $(BCRESULT) \
REAL_RESULT="$(BCRESULT)" make_deps=yes
......@@ -393,14 +400,6 @@ top: $(PRE_TARGETS)
@$(MAKE) -r -f $(OCAMLMAKEFILE) $(TOPRESULT) \
REAL_RESULT="$(BCRESULT)" make_deps=yes
# generates native-code
native-code: $(PRE_TARGETS)
@$(MAKE) -r -f $(OCAMLMAKEFILE) $(NCRESULT) \
REAL_RESULT="$(NCRESULT)" \
REAL_OCAMLC="$(OCAMLOPT)" \
make_deps=yes
nc: native-code
# generates byte-code libraries
byte-code-library: $(PRE_TARGETS)
......@@ -495,15 +494,12 @@ dot:
install:
pushd ../interface ; make; popd ; ../make_lurette ControleurPorte vrai_tram dc
runbug:
./lurette 10 1 1 tram.env usager.env porte.env passerelle.env -ns2c -seed 1013388978
try:
../make_lurette ControleurPorte vrai_tram; \
# ./lurette 10 2 2 tram.env usager.env porte.env passerelle.env | sim2chro -ecran
./lurette 10 2 2 tram.env usager.env porte.env passerelle.env
yvan:
$(LURETTE_DIR)/make_lurette heater Heater_vrai; \
$(LURETTE_PATH)/make_lurette heater Heater_vrai; \
./lurette 50 1 1 Heater.env \
vroum:
......@@ -512,40 +508,40 @@ vroum:
# Non regression test
test:
$(LURETTE_DIR)/make_lurette ControleurPorte; \
./lurette 100 10 10 tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
diff -u ControleurPorte.rif.exp lurette.rif > test1.res ;\
$(LURETTE_PATH)/make_lurette ControleurPorte; \
./lurette 100 10 10 -o tram.rif tram.env usager.env porte.env passerelle.env -seed 1013219512 -ns2c ;\
diff -u ControleurPorte.rif.exp tram.rif > test1.res ;\
\
$(LURETTE_DIR)/make_lurette heater_int; \
./lurette 30 10 10 temp_int.env --no-oracle -seed 1013219512 -ns2c ;\
diff -u heater_int.rif.exp lurette.rif > test2.res ; \
$(LURETTE_PATH)/make_lurette heater_int; \
./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 ; \
\
$(LURETTE_DIR)/make_lurette heater_float; \
./lurette 30 10 10 temp_float.env --no-oracle -seed 1013219512 -ns2c ;\
diff -u heater_float.rif.exp lurette.rif > test3.res ; \
$(LURETTE_PATH)/make_lurette heater_float; \
./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
heater:
$(LURETTE_DIR)/make_lurette heater_int; \
$(LURETTE_PATH)/make_lurette heater_int; \
./lurette 30 1 1 temp_int.env --no-oracle
heaterf:
$(LURETTE_DIR)/make_lurette heater_float; \
$(LURETTE_PATH)/make_lurette heater_float; \
./lurette 30 1 1 temp_float.env --no-oracle
# In order to time profile lurette
gprof:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram pnc; \
$(LURETTE_PATH)/make_lurette ControleurPorte vrai_tram pnc; \
./lurette 4500 1 1 tram.env usager.env porte.env passerelle.env -seed 1014422484 -ns2c ;\
gprof ./lurette > lurette.gprof ; \
echo " ---> The result of the profiling is in the lurette.gprof file"
# In order to time profile lurette
ocamlprof:
$(LURETTE_DIR)/make_lurette heater_float vrai_heater_float pbc; \
$(LURETTE_PATH)/make_lurette heater_float vrai_heater_float pbc; \
./lurette 10 10 10 temp_float.env -ns2c ;\
ocamlprof ../source/solver.ml > prof/solver.count.ml ; \
ocamlprof ../source/wtree.ml > prof/wtree.count.ml ; \
......@@ -578,6 +574,7 @@ docman:
-keep-code -I ../source/ $(SOURCES_OCAML) \
../source/gen_stubs.ml
###########################################################################
# LOW LEVEL RULES
......
interface/Makefile
View file @ 03ffa20e
LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
LURETTE_PATH = /home/jahier/lurette
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
SOURCES = $(LURETTE_DIR)/source/util.ml $(LURETTE_DIR)/source/gen_stubs.ml
SOURCES = $(LURETTE_PATH)/source/util.ml $(LURETTE_PATH)/source/gen_stubs.ml
RESULT = gen_stubs
LIBS = str
......
lurette.prj
View file @ 03ffa20e
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 57)
(Parent-Version lurette 0 56)
(Project-Version lurette 0 58)
(Parent-Version lurette 0 57)
(Version-Log "
Add a --output options to specify the output file name.
Clean up Makefiles for lurette and ima_exe.
Make sure that gen_stubs does not recompile the fake oracle
(always_true.lus) if it is not necessary.
")
(New-Version-Log "")
(Checkin-Time "Thu, 04 Apr 2002 16:06:30 +0200")
(Checkin-Time "Fri, 19 Apr 2002 11:15:07 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -28,7 +31,7 @@ Add a --output options to specify the output file name.
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.34 644))
(source/command_line.ml (lurette/b/20_command_li 1.6 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))
;; Sources files common to lurette and ima_exe
......@@ -70,14 +73,22 @@ Add a --output options to specify the output file name.
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.4 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.7 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.21 644))
(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.22 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.10 744))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.25 644))
(Makefile (lurette/18_Makefile 1.28 644))
(interface/Makefile (lurette/25_Makefile 1.6 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.3 644))
(make_lurette (lurette/27_make_luret 1.9 744))
(OcamlMakefile (lurette/17_OcamlMakef 1.26 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.1 644))
(Makefile.ima_exe (lurette/b/39_Makefile.i 1.1 644))
(test/Makefile (lurette/18_Makefile 1.29 644))
(interface/Makefile (lurette/25_Makefile 1.7 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.4 644))
;; Documentation
......@@ -117,13 +128,6 @@ Add a --output options to specify the output file name.
;; Files added by populate at Mon, 18 Mar 2002 16:20:57 +0100,
;; to version 0.47(w), by jahier:
(source/gne.mli (lurette/b/36_gne.mli 1.1 644))
(source/gne.ml (lurette/b/37_gne.ml 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
make_lurette
View file @ 03ffa20e
#! /bin/sh
#
Help="usage: make_lurette <sut> [<oracle>] <make options>
Usage="usage: make_lurette <sut> [<oracle>] <make options>
The first and second args of this script should respectively be the
name of the sut and the name of the oracle modules (without any
......@@ -17,51 +17,46 @@ lurette Makefile.
"
LURETTE_PATH=/home/jahier/lurette
export LURETTE_PATH
case $# in
##############################################################
[0])
echo "$Help"
echo "$Usage"
exit 0
;;
[1])
echo "... Generates the stub files (gen_stubs $1)"
/home/jahier/lurette/interface/gen_stubs $1
echo "... generates lurette.in file "
rm -f lurette.in
cat << EOF >> lurette.in
SUT = $1.c
ORACLE = always_true.c
export SUT
export ORACLE
EOF
##############################################################
[1])
SUT=`pwd`/$1.c
ORACLE=`pwd`/always_true.c
export SUT
export ORACLE
echo "... Generates the stub files (gen_stubs $1)"
$LURETTE_PATH/interface/gen_stubs $1
echo "... make"
shift 1
make $@
make $@
;;
##############################################################
*)
echo "... Generates the stub files (gen_stubs $1 $2)"
/home/jahier/lurette/interface/gen_stubs $1 $2
echo "... generates lurette.in file "
rm -f lurette.in
cat << EOF >> lurette.in
SUT = $1.c
ORACLE = $2.c
SUT=`pwd`/$1.c
ORACLE=`pwd`/$2.c
export SUT
export ORACLE
export SUT
export ORACLE
echo "... Generates the stub files (gen_stubs $1 $2)"
$LURETTE_PATH/interface/gen_stubs $1 $2
EOF
echo "... make"
shift 2
make $@
make $@
;;
esac
source/command_line.ml
View file @ 03ffa20e
......@@ -30,32 +30,33 @@ type cmd_line_optionT =
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
("--no-step", NoStep);
("--step", Step);
("-s", Step);
("--help", Help);
("-h", Help);
("--verbose", Verbose);
("-v", Verbose);
("--no-oracle", NoOracle);
("--output", Output);
("-o", Output);
("--no-step", NoStep);
("--step", Step);
("-s", Step);
("--with-seed", Seed);
("-seed", Seed);
("-v", Verbose);
("--verbose", Verbose);
("-h", Help);
("--help", Help);
("--no-oracle", NoOracle);
("--call-sim2chro", Sim2chro);
("--do-not-call-sim2chro", NoSim2chro);
("-ns2c", NoSim2chro);
("--display-local-var", DisplayLocalVar);
("--do-not-display-local-var", NoDisplayLocalVar);
("-nlv", NoDisplayLocalVar);
("--call-sim2chro", Sim2chro);
("--do-not-call-sim2chro", NoSim2chro);
("-ns2c", NoSim2chro);
(* ("--init-cudd-heap", CuddHeapInit) *)
]
......@@ -71,7 +72,7 @@ let (option_to_usage: cmd_line_optionT -> string) =
| NoSim2chro -> "Do not call sim2chro when lurette resumes.\n"
(* | CuddHeapInit -> "Set a magic number (related to the gc) that is used by mldd \n\t\t\tfor initializing Dd (Default is 20).\n" *)
| Seed -> "Set the value of the seed the random engine is initialized with (0 lets the system draw a seed).\n"
| NoOracle -> "Do not need to specify an oracle.\n "
| NoOracle -> "Do not run the oracle.\n "
| Verbose -> "Set on a wordier mode.\n"
| Help -> "Print this message.\n"
......
source/gen_stubs.ml
View file @ 03ffa20e
......@@ -879,15 +879,15 @@ let (replace_bool_representation: alias list -> alias list) =
("_boolean", "boolean")::(List.remove_assoc "_boolean" ta)
let update_file new_stub old_stub =
(* Replace old_stub by new_stub iff they are different *)
let update_file new_file old_file =
(* Replace old_file by new_file iff they are different *)
if
not ((Sys.file_exists old_stub)) ||
((Util.readfile old_stub) <> (Util.readfile new_stub))
not ((Sys.file_exists old_file)) ||
((Util.readfile old_file) <> (Util.readfile new_file))
then
if ((Sys.command ("mv " ^ new_stub ^ " " ^ old_stub)) <> 0)
if ((Sys.command ("mv " ^ new_file ^ " " ^ old_file)) <> 0)
then assert false
else print_string ("... " ^ old_stub ^ " successfully created.\n")
else print_string ("... " ^ old_file ^ " successfully created.\n")
let main2 sut oracle =
let sut_h = (sut ^ ".h") in
......@@ -951,7 +951,7 @@ let main2 sut oracle =
generate_lurette_stub_file (get_ml_type sut_vi_ord sut_vo_ord) ;
update_file "lurette_stub.ml.new" "lurette_stub.ml"
(****************************************************************************)
(****************************************************************************)
......@@ -1014,35 +1014,51 @@ let (gen_a_fake_oracle : string -> unit) =
let usage = ("\n\nusage: gen_stub <sut> [<oracle>] \n\twhere <sut> " ^
" (reps <oracle>) is the name of the System Under Test C " ^
" file\n\t(resp the oracle file) without its extension.\n " ^
" The oracle is optional; if omitted, a fake oracle that always " ^
" answers true is generated from <sut>.\n ")
" The oracle is optional; if omitted, a fake oracle that always " ^
" answers true is generated from <sut>.\n ")
(** gen_stubs top-level function *)
let (main : unit -> 'a) =
fun _ ->
try
let sut = Sys.argv.(1) in
let oracle = Sys.argv.(2) in
main2 sut oracle
with Invalid_argument(_) ->
try
let sut = Sys.argv.(1) in
gen_a_fake_oracle sut;
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";
if ((Sys.command ("ec2c always_true.ec")) <> 0)
then failwith "*** ec2c failed. Is it in your path?\n"
else print_string " ... ok\n";
main2 sut "always_true"
with Invalid_argument(_) ->
fun _ ->
let arg_nb = (Array.length Sys.argv) - 1 in
if arg_nb = 0
then
print_string usage
| Sys_error(errMsg) ->
print_string ("\n*** " ^ errMsg ^ "\n") ;
print_string usage
| ecxp ->
raise ecxp
else if arg_nb = 1
then
(
let sut = Sys.argv.(1) in
let old_fake_oracle = Util.readfile "always_true.lus" in
gen_a_fake_oracle sut;
if
( not (Sys.file_exists "always_true.c")
|| not (Sys.file_exists "always_true.h")
|| old_fake_oracle <> (Util.readfile "always_true.lus")