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

lurette 0.52 Thu, 28 Mar 2002 18:10:42 +0100 by jahier

Parent-Version:      0.51
Version-Log:

Remove the necessity to provide an oracle when the user does
not have any assertion to check. To do that, I parse the sut
file and automatically generates a fake oracle that answers always
true.

Project-Description: Lurette
parent 6f6168b0
......@@ -6,30 +6,30 @@
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2978 1016803757 51_env_state. 1.15)
(source/graph.ml 1819 1016011748 14_graph.ml 1.5)
(source/util.ml 10907 1016803757 35_util.ml 1.15)
(source/util.ml 11251 1017335442 35_util.ml 1.16)
(source/wtree.ml 8518 1016011748 b/1_wtree.ml 1.9)
(source/solver.ml 22670 1016803757 39_solver.ml 1.17)
(source/solver.ml 22945 1017335442 39_solver.ml 1.19)
(source/command_line.ml 3998 1016024341 b/20_command_li 1.4)
(source/lurette.ml 11199 1016803757 12_lurette.ml 1.29)
(source/lurette.ml 11217 1017247563 12_lurette.ml 1.30)
(source/solver.mli 1135 1016803757 38_solver.mli 1.10)
(source/env.mli 2517 1016803757 15_env.mli 1.10)
(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 10689 1016803757 16_env.ml 1.20)
(make_lurette 812 1013517738 27_make_luret 1.7)
(source/env.ml 10994 1017247563 16_env.ml 1.21)
(make_lurette 1149 1017335442 27_make_luret 1.8)
(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 925 1017156165 b/17_passerelle 1.4)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 10788 1016803757 b/27_rnumsolver 1.4)
(source/rnumsolver.ml 10794 1017335442 b/27_rnumsolver 1.5)
(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/ima_exe.ml 7152 1016803757 b/32_ima_exe.ml 1.2)
(source/ima_exe.ml 7153 1017247563 b/32_ima_exe.ml 1.3)
(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 33406 1016803757 24_generate_l 1.20)
(source/parse_env.ml 13888 1017232599 41_parse_env. 1.12)
(source/gen_stubs.ml 35425 1017335442 24_generate_l 1.21)
(source/parse_env.ml 15579 1017247563 41_parse_env. 1.13)
(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)
......@@ -41,12 +41,12 @@
(source/wtree.mli 2340 1016011748 b/0_wtree.mli 1.7)
(test/porte.env 950 1017156165 b/16_porte.env 1.4)
(source/env_state.mli 3851 1016803757 50_env_state. 1.13)
(source/rnumsolver.mli 1758 1016803757 b/26_rnumsolver 1.2)
(source/rnumsolver.mli 1764 1017335442 b/26_rnumsolver 1.3)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(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 19280 1016127950 17_OcamlMakef 1.22)
(OcamlMakefile 19266 1017335442 17_OcamlMakef 1.24)
(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 990 1017156165 b/15_tram.env 1.4)
......@@ -58,7 +58,7 @@
(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
(source/gne.ml 8204 1016803757 b/37_gne.ml 1.1)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1756 1016803757 18_Makefile 1.24)
(Makefile 1837 1017335442 18_Makefile 1.25)
(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)
......
......@@ -11,7 +11,7 @@ INCDIRS = /home/jahier/include
LIBDIRS = /home/jahier/lib
# Requires cudd and mldd to be installed!
LIBS = nums # mlpoly
LIBS = str nums # mlpoly
CLIBS = cudd_caml cuddaux cudd mtr st epd util # libppl libpolyi
USE_CAMLP4 = yes
......@@ -20,6 +20,8 @@ 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 \
......
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.23 Wed, 27 Mar 2002 17:46:03 +0100 jahier $
# $Id: OcamlMakefile 1.24 Thu, 28 Mar 2002 18:10:42 +0100 jahier $
#
###########################################################################
......@@ -512,15 +512,15 @@ vroum:
# Non regression test
test:
$(LURETTE_DIR)/make_lurette ControleurPorte vrai_tram; \
$(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_DIR)/make_lurette heater_int vrai_heater; \
$(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_DIR)/make_lurette heater_float vrai_heater_float; \
$(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 ; \
\
......@@ -529,11 +529,11 @@ test:
heater:
$(LURETTE_DIR)/make_lurette heater_int vrai_heater; \
$(LURETTE_DIR)/make_lurette heater_int; \
./lurette 30 1 1 temp_int.env --no-oracle
heaterf:
$(LURETTE_DIR)/make_lurette heater_float vrai_heater_float; \
$(LURETTE_DIR)/make_lurette heater_float; \
./lurette 30 1 1 temp_float.env --no-oracle
# In order to time profile lurette
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 51)
(Parent-Version lurette 0 50)
(Project-Version lurette 0 52)
(Parent-Version lurette 0 51)
(Version-Log "
Change the way pre are translated in the .env file. Now
instead of writting \"_pre2toto\", one writes \"pre(2,toto)\".
But internally, it is handled the same way as before (i.e., the first
thing I do when parsing the env file is to transform \"pre(2,toto)\"
into \"_pre2toto\" (it makes the hangling of pre vars much more
homogeneous with the way the other vars are handled.
Also fix a bug where it was not possible to have a pre on input
vars because the update_pre was failing to proceed quietly whenever
one of its var was not computable because its pre does have a value.
Also give an appropriate error message whenever the user wrongly
use a pre on a var that can not be computed.
Remove the necessity to provide an oracle when the user does
not have any assertion to check. To do that, I parse the sut
file and automatically generates a fake oracle that answers always
true.
")
(New-Version-Log "")
(Checkin-Time "Wed, 27 Mar 2002 17:46:03 +0100")
(Checkin-Time "Thu, 28 Mar 2002 18:10:42 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -51,13 +41,13 @@ use a pre on a var that can not be computed.
(source/env.mli (lurette/15_env.mli 1.10 644))
(source/env.ml (lurette/16_env.ml 1.21 644))
(source/util.ml (lurette/35_util.ml 1.15 644))
(source/util.ml (lurette/35_util.ml 1.16 644))
(source/solver.mli (lurette/38_solver.mli 1.10 644))
(source/solver.ml (lurette/39_solver.ml 1.18 644))
(source/solver.ml (lurette/39_solver.ml 1.19 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.2 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.4 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.3 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.5 644))
(source/parse_env.mli (lurette/40_parse_env. 1.6 644))
(source/parse_env.ml (lurette/41_parse_env. 1.13 644))
......@@ -83,14 +73,14 @@ use a pre on a var that can not be computed.
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.3 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.6 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.20 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.21 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.23 644))
(Makefile (lurette/18_Makefile 1.24 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.24 644))
(Makefile (lurette/18_Makefile 1.25 644))
(interface/Makefile (lurette/25_Makefile 1.6 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.2 644))
(make_lurette (lurette/27_make_luret 1.7 744))
(make_lurette (lurette/27_make_luret 1.8 744))
;; Documentation
......
#! /bin/sh
#
Help="usage: make_lurette <sut> <oracle> <make options>
Help="usage: make_lurette <sut> [<oracle>] <make options>
The first and second args of this scripts should respectively be the
name of the sut and the name of the oracle modules (without any
extension).
extension). Note that the oracle is optional.
1) It calls the gen_stubs script to generate stub files to interface
the C (poc) files implementing the sut and the oracle with lurette.
......@@ -18,10 +18,31 @@ lurette Makefile.
"
case $# in
[01])
[0])
echo "$Help"
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
echo "... make"
shift 1
make $@
;;
*)
echo "... Generates the stub files (gen_stubs $1 $2)"
/home/jahier/lurette/interface/gen_stubs $1 $2
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: generate_lurette_interface.ml
** File: gen_stubs.ml
** Main author: jahier@imag.fr
**
*)
(** Generates stubs for calling poc C programs with lurette. It takes as
input the string "sut" (resp. "oracle") as well as a C header file
[<foo>.h] to interface, and outputs stub files named [lurette_sut.h] and
[lurette_sut.c] (resp. [lurette_oracle.h] and [lurette_oracle.c]).
Those files are used by the lurette Makefile to interface the sut
(resp. the oracle).
(** 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.
Note that <foo>.h should follows the poc convention (e.g., generated
by a lustre compiler). Namely, it should contain the following pragmas:
Note that the C files should follows the poc convention (e.g., generated
by a lustre compiler). For instance, the header files should contain
the following pragmas:
//MODULE: <module name> n m
//MODULE: <module name> n m
(* where [n] is the input var number, and [m] the output var one *)
//IN: <C type of the first input var> <a C identifier for the first input var>
//IN: <C type of the first input var> <a C identifier for the first input var>
...
...
//IN: <C type of the nth input var> <a C identifier for the nth input var>
//OUT: <C type of the first output var> <a C identifier for the first output var>
//IN: <C type of the nth input var> <a C identifier for the nth input var>
//OUT: <C type of the first output var> <a C identifier for the first output var>
...
//OUT: <C type of the mth output var> <a C identifier for the mth output var>
//OUT: <C type of the mth output var> <a C identifier for the mth output var>
*)
(****************************************************************************)
......@@ -64,13 +62,13 @@ let reg_semicol = Str.regexp ";"
type alias = c_type * c_type
(**
[get_typedef_alias file] reads [file] (a C header file) and search
for typedef C expressions and returns the list of (alias_type, C_type)
found in [file].
*)
let rec
(get_typedef_alias: file -> alias list) =
(*
** [get_typedef_alias file] reads [file] (a C header file) and search
** for typedef C expressions and returns the list of (alias_type, C_type)
** found in [file].
*)
fun file ->
let str = Util.readfile file in
find_typedef_list str 0 []
......@@ -108,26 +106,30 @@ let reg_IN = Str.regexp "^//IN:"
let reg_OUT = Str.regexp "^//OUT:"
let reg_cr = Str.regexp "\n"
let rec (get_vn_and_ct_list: file -> module_name * vn_ct list * vn_ct list) =
(*
** Parses poc pragmas in a C header file and returns the module name, the
** list of input vars, and the list of output vars name and type.
**
** poc pragmas have the following shape:
**
** //MODULE: <module name> n m
** (* where [n] is the input var number, and [m] the output var one *)
** //IN: <C type of the first input var> <a C identifier for the first input var>
** .
** .
** .
** //IN: <C type of the nth input var> <a C identifier for the nth input var>
** //OUT: <C type of the first output var> <a C identifier for the first output var>
** .
** .
** .
** //OUT: <C type of the mth output var> <a C identifier for the mth output var>
(**
Parses poc pragmas in a C header file and returns the module name, the
list of input vars, and the list of output vars name and type.
poc pragmas have the following shape:
//MODULE: <module name> n m
(* where [n] is the input var number, and [m] the output var one *)
//IN: <C type of the first input var> <a C identifier for the first input var>
...
//IN: <C type of the nth input var> <a C identifier for the nth input var>
//OUT: <C type of the first output var> <a C identifier for the first output var>
...
//OUT: <C type of the mth output var> <a C identifier for the mth output var>
*)
let rec (get_vn_and_ct_list: file -> module_name * vn_ct list * vn_ct list) =
fun file ->
let str = Util.readfile file in
let (mod_name, ni, no, str_ptr1) = find_module_name str in
......@@ -197,6 +199,7 @@ let _ = match (get_vn_and_ct_list "tram_simple.h") with
(****************************************************************************)
(****************************************************************************)
(** 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
......@@ -212,11 +215,11 @@ let _ = assert (
type res = Ok | Error of string
let (check_var_type: vn_ct list -> vn_ct list -> vn_ct list -> res) =
(*
** [check_var_type sut_vars or_vi or_vo] checks the consistency
** of variable names and types of the sut and the oracle.
(**
[check_var_type sut_vars or_vi or_vo] checks the consistency
of variable names and types of the sut and the oracle.
*)
let (check_var_type: vn_ct list -> vn_ct list -> vn_ct list -> res) =
fun sut_vars or_vi or_vo ->
let print_var_list vl =
List.iter
......@@ -258,11 +261,11 @@ let _ = assert ((check_var_type
(****************************************************************************)
(****************************************************************************)
let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit) =
(*
** [generate_stub_c mod_name str vi vo] generates a file named [<str>_stub.c]
** that interfaces the sut and the oracle with Lurette.
(**
[generate_stub_c mod_name str vi vo] generates a file named [<str>_stub.c]
that interfaces the sut and the oracle with Lurette.
*)
let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit) =
fun mod_name str vi vo ->
let oc = open_out (str ^ "_stub.c.new") in
let put s = output_string oc s in
......@@ -358,13 +361,13 @@ let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit)
type sut_or_oracle = string
(**
[generate_idl mod_name str vi vo] generates an idl file named
[<str>_idl_stub.idl] that camlidl processes to generate stub files that
will interface C poc files with lurette.
*)
let (generate_idl : module_name -> sut_or_oracle -> vn_ct list -> vn_ct list
-> unit) =
(*
** [generate_idl mod_name str vi vo] generates an idl file named
** [<str>_idl_stub.idl] that camlidl processes to generate stub files that
** will interface C poc files with lurette.
*)
fun mod_name str vi vo ->
let oc = open_out (str ^ "_idl_stub.idl.new") in
let put s = output_string oc s in
......@@ -417,10 +420,10 @@ let (generate_idl : module_name -> sut_or_oracle -> vn_ct list -> vn_ct list
(****************************************************************************)
(****************************************************************************)
(**
[generate_n_var_names "x" 4] generates the list ["x1"; "x2"; "x3"; "x4"]
*)
let rec (generate_n_var_names: string -> int -> fresh_var_name list) =
(*
** [generate_n_var_names "x" 4] generates the list ["x1"; "x2"; "x3"; "x4"]
*)
fun x n ->
match n with
0 -> []
......@@ -432,8 +435,8 @@ 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) =
(* cf get_ml_type *)
fun file lin lout ->
let str = Util.readfile file in
let reg_external = Str.regexp "^external sut_step :" in
......@@ -538,21 +541,21 @@ let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_c
(generate_n_var_names "y" (List.length lout)))
)
let (get_ml_type: vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_ct_mlt_fvn list) =
(*
** [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
** the input vars, the 2nd one for the output ones) of tuples containing
** a var name, its ml type, as well as a fresh variable name that will be
** used later.
(**
[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
the input vars, the 2nd one for the output ones) of tuples containing
a var name, its ml type, as well as a fresh variable name that will be
used later.
*)
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
(*
** interface/sut_idl_stub.ml has been defined to be able to check that
** assertion.
(**
interface/sut_idl_stub.ml has been defined to be able to check that
assertion.
*)
let _ = assert
( (get_ml_type2 "/home/jahier/lurette/interface/sut_idl_stub.ml"
......@@ -566,36 +569,37 @@ let _ = assert
(****************************************************************************)
(****************************************************************************)
let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit) =
(*
** [generate_lurette_stub_file sut_vi sut_vo] generates an ocaml file that defines:
** - the type of sut inputs (as a tuple containing the sut variables
** ordered lexicographically w.r.t. their names)
** - the type of sut outputs (in the same manner)
** - Defines a version of [sut_try] that takes as argument a tuple
** instead of a currified list of input values as camlidl provides.
** - ditto for [sut_step], [oracle_try], and [oracle_step]
** - a list of sut (input and output) variable names and types (so that
** we can check later that the environment variable names and types are
** consistent with the ones of the sut).
** - 2 functions (lookup_sut_in and lookup_sut_out) to access a value from
** the input and output tuples given a variable name.
(** Formats list of strings. E.g., [format_string_list " * " ["int";
"bool"; "float"]] returns the string "int * bool * float".
*)
let rec (format_string_list: string -> string list -> string) =
fun str list ->
match list with
[] -> ""
| [e] -> e
| e::t -> (e ^ str ^ (format_string_list str t))
(**
[generate_lurette_stub_file sut_vi sut_vo] generates an ocaml file that defines:
- the type of sut inputs (as a tuple containing the sut variables
ordered lexicographically w.r.t. their names)
- the type of sut outputs (in the same manner)
- Defines a version of [sut_try] that takes as argument a tuple
instead of a currified list of input values as camlidl provides.
- ditto for [sut_step], [oracle_try], and [oracle_step]
- a list of sut (input and output) variable names and types (so that
we can check later that the environment variable names and types are
consistent with the ones of the sut).
- 2 functions (lookup_sut_in and lookup_sut_out) to access a value from
the input and output tuples given a variable name.
*)
let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit) =
fun (sut_in, sut_out) ->
let oc = open_out "lurette_stub.ml.new" in
let put s = output_string oc s in
let rec (format_string_list: string -> string list -> string) =
(*
** [format_string_list " * " ["int"; "bool"; "float"]] returns the string
** "int * bool * float".
*)
fun str list ->
match list with
[] -> ""
| [e] -> e
| e::t -> (e ^ str ^ (format_string_list str t))
in
let _ = assert ((format_string_list " * " ["int"; "bool"; "float"])
= "int * bool * float")
in
......@@ -866,11 +870,11 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
(****************************************************************************)
(****************************************************************************)
(**
Lustre defines [_boolean] as an [int], but camlidl maps C [boolean]
to the caml [bool] type.
*)
let (replace_bool_representation: alias list -> alias list) =
(*
** Lustre defines [_boolean] as an [int], but camlidl maps C [boolean]
** to the caml [bool] type.
*)
fun ta ->
("_boolean", "boolean")::(List.remove_assoc "_boolean" ta)
......@@ -951,11 +955,70 @@ let main2 sut oracle =
(****************************************************************************)
(****************************************************************************)
let usage = ("\n\nusage: gen_stub <sut> <oracle> \n\twhere <sut> " ^
(** Translates C-poc type into lustre type *)
let c_type_to_lustre_type ct =
(* I know what a poc C file generated by lustre looks like, but what
about poc files coming from esterel ??
*)
if Util.is_substring "int" ct
then "int"
else if ((Util.is_substring "float" ct) || (Util.is_substring "real" ct))
then "real"
else if Util.is_substring "bool" ct
then "bool"
else
(
print_string ("*** I don't know that type, sorry. It should work if "
^ "you provide your own oracle however.\n");
flush stdout;
assert false
)
(** Generates a fake oracle (that always answers true) so that the
user does not have to write it if he does not have any assertion to
check.
*)
let (gen_a_fake_oracle : string -> unit) =
fun sut ->
let sut_h = (sut ^ ".h") in
let (sut_m, sut_vi, sut_vo) = get_vn_and_ct_list sut_h in
let vn_lt_l =
List.map
(fun (vn, ct) -> (vn, (c_type_to_lustre_type ct)))
(List.append sut_vi sut_vo)
in
let vn_lt_str_l =
List.map (fun (vn, lt) -> (vn ^ ":" ^ lt)) vn_lt_l
in
let oc = open_out "always_true.lus" in
let put s = output_string oc s in
put "-- Automatically generated from ";
put sut_h ;
put " by interface/gen_stubs. \n" ;
put "\n";
put "node always_true(";
put (format_string_list "; " vn_lt_str_l) ;
put ") returns (ok:bool);\n";
put "let \n ok = true ; \ntel\n";
put "\n";
close_out oc
(****************************************************************************)
(****************************************************************************)
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 ")
" 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 ")
(** gen_stubs top-level function *)
let (main : unit -> 'a) =
fun _ ->
try
......@@ -963,11 +1026,22 @@ let (main : unit -> 'a) =
let oracle = Sys.argv.(2) in
main2 sut oracle
with Invalid_argument(_) ->
print_string usage
| Sys_error(errMsg) ->
print_string ("\n*** " ^ errMsg ^ "\n") ;
print_string usage
| ecxp ->
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(_) ->
print_string usage