diff --git a/.ocaml-config.sh b/.ocaml-config.sh
deleted file mode 100755
index 76fd574e4f51a2a7c89423c816c09061bfa7196c..0000000000000000000000000000000000000000
--- a/.ocaml-config.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/bin/sh
-case "$OCAML_VERSION,$OPAM_VERSION" in
- 4.01.0,1.1.0) ppa=avsm/ocaml41+opam11 ;;
- 4.01.0,1.2.0) ppa=avsm/ocaml41+opam12 ;;
- 4.02.1,1.1.0) ppa=avsm/ocaml42+opam11 ;;
- 4.02.1,1.2.0) ppa=avsm/ocaml42+opam12 ;;
- *) echo Unknown $OCAML_VERSION,$OPAM_VERSION; exit 1 ;;
-esac
-
-echo "\n" | add-apt-repository ppa:$ppa
diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
index 13bb75275f848f3e13ba92d3d1ad3c1a013deb9a..0000000000000000000000000000000000000000
--- a/.travis.yml
+++ /dev/null
@@ -1,60 +0,0 @@
-language: c
-env:
- - OCAML_VERSION=4.02.1 OPAM_VERSION=1.2.0
- - OCAML_VERSION=4.01.0 OPAM_VERSION=1.2.0
-
-before_install:
- - until sudo add-apt-repository -y ppa:saiarcot895/chromium-beta; do echo retry; done
- - until sudo add-apt-repository --yes ppa:kalakris/cmake; do echo retry; done
- - until sudo apt-get -qq update; do echo retry; done
- - until sudo apt-get install cmake; do echo retry; done
- - OPAM_DEPENDS="ocamlgraph ocamlfind"
- - chmod +x ./.ocaml-config.sh
- - sudo -E ./.ocaml-config.sh
-
-install:
- - sudo apt-get update -qq
- - sudo apt-get install -qq ocaml opam
- - export OPAMYES=1
- - opam init
- - opam install ${OPAM_DEPENDS}
- - eval `opam config env`
- - export LZ="$TRAVIS_BUILD_DIR/../zustre"
- - git clone https://github.com/coco-team/zustre $LZ
- - ls $LZ
- - export Z3="$TRAVIS_BUILD_DIR/../z3"
- - mkdir -p $Z3
- - wget --output-document=zustre.tar.gz https://www.dropbox.com/s/9cvef743630rten/zustre.tar.gz?dl=1;
- - tar xvf zustre.tar.gz --strip-components=1 -C $Z3;
- - ls $LZ
- - ls $Z3
-
-before_script:
- - ocaml -version
- - opam --version
-
-script:
- - autoconf
- - ./configure
- - make
- - ./bin/lustrec
- - cd $LZ
- - mkdir -p build
- - cd build
- - /usr/bin/cmake -DLUSTREC_EXECUTABLE=/home/travis/build/coco-team/lustrec/bin/lustrec -DZ3_ROOT=$Z3 -DCMAKE_BUILD_TYPE=Release -DCMAKE_INSTALL_PREFIX=run -DCMAKE_PROGRAM_PATH=/usr/bin ../;
- - /usr/bin/cmake --build .
- - /usr/bin/cmake --build . --target install
- - cd ..
- - ls build/run/bin
- - ./build/run/bin/zustre -h
- - python src/reg_test.py ./build/run/bin/zustre
-
-
-
-
-notifications:
- email:
- recipients:
- - lustrec-build@googlegroups.com
- on_success: always
- on_failure: always
diff --git a/dune-project b/dune-project
index 70d26124bbd403a98e13dfe82a49c02d114cab43..ce248dca8155c08c1217032a2a06d93f5df8b161 100644
--- a/dune-project
+++ b/dune-project
@@ -28,5 +28,12 @@
of Simulink models. Within CocoSim, the Lustre language is used as an \
intermediate representation and relies mainly on lustrec to produce code \
or verification artifacts.")
- (depends ocamlgraph menhir zarith dune-site)
- (depopts z3 yojson))
+ (depends
+ ocamlgraph
+ menhir
+ zarith
+ yojson
+ ppx_deriving_yojson
+ ; cmdliner
+ dune-site)
+ (depopts z3))
diff --git a/lustrec.opam b/lustrec.opam
index 8c76442c8cf661b008a7884518a48018d503a712..dc5a64ea2022dbf429ace3902604218c6e01b040 100644
--- a/lustrec.opam
+++ b/lustrec.opam
@@ -17,10 +17,12 @@ depends: [
"ocamlgraph"
"menhir"
"zarith"
+ "yojson"
+ "ppx_deriving_yojson"
"dune-site"
"odoc" {with-doc}
]
-depopts: ["z3" "yojson"]
+depopts: ["z3"]
build: [
["dune" "subst"] {dev}
[
diff --git a/opam.in b/opam.in
deleted file mode 100644
index ead3cbcd785ce5367cab6ac11fbbee656680cdac..0000000000000000000000000000000000000000
--- a/opam.in
+++ /dev/null
@@ -1,44 +0,0 @@
-opam-version: "2.0"
-name: "lustrec"
-version: "@VERSION_NUMBER@"
-maintainer: "Pierre-Loic Garoche <ploc@garoche.net>"
-authors: ["Pierre-Loic Garoche <ploc@garoche.net>" "Xavier Thirioux <thirioux@enseeiht.fr>"]
-homepage: "https://cavale.enseeiht.fr/redmine/projects/lustrec/"
-bug-reports: "https://cavale.enseeiht.fr/redmine/projects/lustrec/issues"
-license: "LGPL"
-dev-repo: "git+https://cavale.enseeiht.fr/git/lustrec#unstable"
-build: [
- ["autoconf"]
- ["./configure" "--prefix=%{prefix}%"]
- [make]
-]
-install: [make "install"]
-remove: [make "uninstall"]
-depends: [
- "ocamlfind"
- "yojson"
- "cmdliner"
- "fmt"
- "ppx_deriving_yojson"
- "ppx_traverse_builtins"
- "ppxlib"
- "menhir"
- "ocamlgraph"
- "logs"
- "z3"
- "num"
-]
-synopsis: "A Lustre compiler toolset"
-description: """
-lustrec is structured around the modular compilation scheme proposed
-by Biernacki, Colaço, Hamon, and Pouzet at LCTES'08. It is an open
-source lustre compiler that provides verification capabilities.
-It is currently mainly used through the CocoSim platform, a Matlab
-toolbox to perform V&V of Simulink models. Within CocoSim, the Lustre
-language is used as an intermediate representation and relies mainly
-on lustrec to produce code or verification artifacts.
-"""
-url {
- src: "https://cavale.enseeiht.fr/redmine/attachments/download/117/lustrec-1.6-Xia-Zhu-src.tgz"
- checksum: "md5=f06e87d5fbb24c91894bdc55bf6cc496"
-}
diff --git a/src/automata.ml b/src/automata.ml
index 97686e04b92cc519f6de4d800b48eddb2aa81707..e5388d9f305f64dc06a77098d3f3e48b91863b7e 100644
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -67,7 +67,7 @@ let mkautomata loc id handlers =
let expr_of_exit loc restart state conds tag =
mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
-let rec unless_read reads handler =
+let unless_read reads handler =
let res =
List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_unless
in
@@ -79,7 +79,7 @@ Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list ~sep:"
res
)
-let rec until_read reads handler =
+let until_read reads handler =
List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_until
let rec handler_read reads handler =
@@ -136,7 +136,7 @@ let mkautomata_state nodeid used typedef loc id =
let vars_of_aut_state aut_state =
[aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s]
-let node_of_unless nused used node aut_id aut_state handler =
+let node_of_unless nused node aut_id aut_state handler =
(*Format.eprintf "node_of_unless %s@." node.node_id;*)
let inputs = unless_read ISet.empty handler in
let var_inputs = aut_state.incoming_r (*:: aut_state.incoming_s*) :: (node_vars_of_idents node inputs) in
@@ -228,13 +228,13 @@ let typedef_of_automata aut =
let expand_automata nused used owner typedef node aut =
let initial = (List.hd aut.aut_handlers).hand_state in
let aut_state = mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id in
- let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in
+ let unodes = List.map (fun h -> node_of_unless nused node aut.aut_id aut_state h) aut.aut_handlers in
let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in
let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in
- let unless_handlers = List.map2 (fun h (n, c) -> (h.hand_state, c)) aut.aut_handlers unodes in
+ let unless_handlers = List.map2 (fun h (_, c) -> (h.hand_state, c)) aut.aut_handlers unodes in
let unless_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.incoming_s.var_id, unless_handlers)) in
let unless_eq = mkeq aut.aut_loc ([aut_state.actual_r.var_id; aut_state.actual_s.var_id], unless_expr) in
- let assign_until_handlers = List.map2 (fun h (_, n, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in
+ let assign_until_handlers = List.map2 (fun h (_, _, c) -> (h.hand_state, c)) aut.aut_handlers aunodes in
let assign_until_expr = mkexpr aut.aut_loc (Expr_merge (aut_state.actual_s.var_id, assign_until_handlers)) in
let assign_until_vars = [aut_state.incoming_r'.var_id; aut_state.incoming_s'.var_id] @ (ISet.elements all_outputs) in
let assign_until_eq = mkeq aut.aut_loc (assign_until_vars, assign_until_expr) in
diff --git a/src/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml
index 1e7a2635d2245e9a1d4277192f83584f29bf26b2..4a364a8a622ec18953a3b63fb08063dcdd32cef2 100644
--- a/src/backends/Ada/ada_backend.ml
+++ b/src/backends/Ada/ada_backend.ml
@@ -13,7 +13,6 @@ open Format
open Machine_code_types
open Misc_lustre_function
-open Ada_printer
open Ada_backend_common
let indent_size = 2
@@ -71,7 +70,7 @@ let get_typed_submachines machines m =
let extract_contract machines m =
let rec find_submachine_from_ident ident = function
| [] -> raise Not_found
- | h::t when h.mname.node_id = ident -> h
+ | h::_ when h.mname.node_id = ident -> h
| _::t -> find_submachine_from_ident ident t
in
let extract_ident eexpr =
@@ -119,18 +118,16 @@ let extract_contract machines m =
(** Main function of the Ada backend. It calls all the subfunction creating all
the file and fill them with Ada code representing the machines list given.
@param basename name of the lustre file
- @param prog useless
@param prog list of machines to translate
- @param dependencies useless
**)
-let translate_to_ada basename prog machines dependencies =
+let translate_to_ada basename machines =
let module Ads = Ada_backend_ads.Main in
let module Adb = Ada_backend_adb.Main in
let module Wrapper = Ada_backend_wrapper.Main in
let is_real_machine m =
match m.mspec with
- | Some (Contract x) -> false
+ | Some (Contract _) -> false
| _ -> true
in
@@ -176,10 +173,22 @@ let translate_to_ada basename prog machines dependencies =
(match main_machine with
| None -> ()
| Some machine ->
- write_file destname pp_main_filename (Wrapper.pp_main_adb (get_typed_submachines filtered_machines machine)) machine;
- write_file destname (Wrapper.pp_project_name (basename^"_exe")) (Wrapper.pp_project_file filtered_machines basename) main_machine);
- write_file destname Wrapper.pp_project_configuration_name Wrapper.pp_project_configuration_file basename;
- write_file destname (Wrapper.pp_project_name (basename^"_lib")) (Wrapper.pp_project_file filtered_machines basename) None;
+ write_file destname
+ pp_main_filename
+ (Wrapper.pp_main_adb (*get_typed_submachines filtered_machines machine*))
+ machine;
+ write_file destname
+ (fun fmt _ -> Wrapper.pp_project_name (basename^"_exe") fmt)
+ (Wrapper.pp_project_file filtered_machines basename)
+ main_machine);
+ write_file destname
+ Wrapper.pp_project_configuration_name
+ (fun fmt _ -> Wrapper.pp_project_configuration_file fmt)
+ basename;
+ write_file destname
+ (fun fmt _ -> Wrapper.pp_project_name (basename^"_lib") fmt)
+ (Wrapper.pp_project_file filtered_machines basename)
+ None;
(* Local Variables: *)
diff --git a/src/backends/Ada/ada_backend_adb.ml b/src/backends/Ada/ada_backend_adb.ml
index d962b00ad5db54bde2a0c30f0fb4a27b057abffe..a34caf96b13a106f93960dd9fc2b58b5b4c8510d 100644
--- a/src/backends/Ada/ada_backend_adb.ml
+++ b/src/backends/Ada/ada_backend_adb.ml
@@ -129,7 +129,7 @@ struct
| MLocalAssign (ident, value) ->
{ instr_desc = MStateAssign (ident, value);
lustre_eq= instr.lustre_eq }
- | x -> instr
+ | _ -> instr
in
let pp_local_ghost_list, spec_instrs = match m_spec_opt with
| None -> [], []
@@ -154,7 +154,7 @@ struct
in
let env, memory = match m_spec_opt with
| None -> env, m.mmemory
- | Some m_spec ->
+ | Some _ ->
env,
(m.mmemory)
in
diff --git a/src/backends/Ada/ada_backend_ads.ml b/src/backends/Ada/ada_backend_ads.ml
index 8a306c687f6bbd32b8381a047dbdf2b6d0276c3c..848b199030ff6f6905659fe269f21bcb1dd918e9 100644
--- a/src/backends/Ada/ada_backend_ads.ml
+++ b/src/backends/Ada/ada_backend_ads.ml
@@ -13,10 +13,7 @@ open Format
open Machine_code_types
open Lustre_types
-open Corelang
-open Machine_code_common
-open Misc_printer
open Misc_lustre_function
open Ada_printer
open Ada_backend_common
@@ -39,9 +36,8 @@ struct
(** Print the expression function representing the transition predicate.
@param fmt the formater to print on
- @param machine the machine
**)
- let pp_init_predicate typed_submachines fmt (opt_spec_machine, m) =
+ let pp_init_predicate fmt () =
let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
pp_predicate pp_init_name [[new_state]] true fmt None
@@ -49,14 +45,14 @@ struct
@param fmt the formater to print on
@param machine the machine
**)
- let pp_transition_predicate typed_submachines fmt (opt_spec_machine, m) =
+ let pp_transition_predicate fmt (_, m) =
let old_state = (AdaIn, pp_state_name_predicate suffixOld, pp_state_type, None) in
let new_state = (AdaIn, pp_state_name_predicate suffixNew, pp_state_type, None) in
let inputs = build_pp_var_decl_step_input AdaIn None m in
let outputs = build_pp_var_decl_step_output AdaIn None m in
pp_predicate pp_transition_name ([[old_state; new_state]]@inputs@outputs) true fmt None
- let pp_invariant_predicate typed_submachines fmt (opt_spec_machine, m) =
+ let pp_invariant_predicate fmt () =
pp_predicate pp_invariant_name [[build_pp_state_decl AdaIn None]] true fmt None
(** Print a new statement instantiating a generic package.
@@ -204,12 +200,11 @@ struct
(pp_package (pp_axiomatize_package_name) [] false)
(fun fmt -> fprintf fmt "pragma Annotate (GNATProve, External_Axiomatization);@,@,%a;@,%a;@,%a"
(*Declare the init predicate*)
- (pp_init_predicate typed_submachines) (m_spec_opt, m)
+ pp_init_predicate ()
(*Declare the transition predicate*)
- (pp_transition_predicate typed_submachines) (m_spec_opt, m)
+ pp_transition_predicate (m_spec_opt, m)
(*Declare the invariant predicate*)
- (pp_invariant_predicate typed_submachines) (m_spec_opt, m)
- )
+ pp_invariant_predicate ())
(*Print the private section*)
pp_private_section
diff --git a/src/backends/Ada/ada_backend_common.ml b/src/backends/Ada/ada_backend_common.ml
index 34a4b64c6ffc923ae3a59a8939209df8e2f400e3..68a5228d93b04572b289a0e83812fd447e6c51fc 100644
--- a/src/backends/Ada/ada_backend_common.ml
+++ b/src/backends/Ada/ada_backend_common.ml
@@ -2,7 +2,6 @@ open Format
open Machine_code_types
open Lustre_types
-open Corelang
open Machine_code_common
open Ada_printer
@@ -16,27 +15,33 @@ exception Ada_not_supported of string
@param fmt the formater to print on
**)
let pp_state_name fmt = fprintf fmt "state"
+
(** Print the type of the state variable.
@param fmt the formater to print on
**)
let pp_state_type fmt = fprintf fmt "TState"
-(** Print the name of the reset procedure
+
+ (** Print the name of the reset procedure
@param fmt the formater to print on
**)
let pp_reset_procedure_name fmt = fprintf fmt "reset"
-(** Print the name of the step procedure
+
+ (** Print the name of the step procedure
@param fmt the formater to print on
**)
let pp_step_procedure_name fmt = fprintf fmt "step"
-(** Print the name of the main procedure.
+
+ (** Print the name of the main procedure.
@param fmt the formater to print on
**)
let pp_main_procedure_name fmt = fprintf fmt "ada_main"
-(** Print the name of the arrow package.
+
+ (** Print the name of the arrow package.
@param fmt the formater to print on
**)
let pp_arrow_package_name fmt = fprintf fmt "Arrow"
-(** Print the type of a polymorphic type.
+
+ (** Print the type of a polymorphic type.
@param fmt the formater to print on
@param id the id of the polymorphic type
**)
@@ -282,7 +287,7 @@ let pp_basic_lib_fun pp_value ident fmt vl =
Format.fprintf fmt "(if %a then %a else %a)" pp_value v1 pp_value v2 pp_value v3
| op, [v1; v2] ->
Format.fprintf fmt "(%a %s %a)" pp_value v1 op pp_value v2
- | op, [v1] when List.mem_assoc ident ada_supported_funs ->
+ | _, [v1] when List.mem_assoc ident ada_supported_funs ->
let pkg, name = try List.assoc ident ada_supported_funs
with Not_found -> assert false in
let pkg = pkg^(if String.equal pkg "" then "" else ".") in
@@ -368,8 +373,7 @@ let build_pp_arg_reset m =
@ (build_pp_var_decl_static AdaIn None m)
-let build_pp_arg_transition m =
- (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
- @ (build_pp_var_decl_step_input AdaIn None m)
- @ (build_pp_var_decl_step_output AdaOut None m)
-
+(* let build_pp_arg_transition m =
+ * (if is_machine_statefull m then [[build_pp_state_decl AdaInOut None]] else [])
+ * @ (build_pp_var_decl_step_input AdaIn None m)
+ * @ (build_pp_var_decl_step_output AdaOut None m) *)
diff --git a/src/backends/Ada/ada_backend_wrapper.ml b/src/backends/Ada/ada_backend_wrapper.ml
index ea5c15d8e641fc9e93895a5cc16c3b1e1de09a96..90b5b7f16bab7fd584c8bb3b1a01b601d94b0ccc 100644
--- a/src/backends/Ada/ada_backend_wrapper.ml
+++ b/src/backends/Ada/ada_backend_wrapper.ml
@@ -32,7 +32,7 @@ struct
@param fmt the formater to print on
@param machine the main machine
**)
- let pp_main_adb typed_submachines fmt machine =
+ let pp_main_adb fmt machine =
let statefull = is_machine_statefull machine in
let pp_package = pp_package_name_with_polymorphic [] machine in
@@ -102,17 +102,15 @@ struct
(** Print the project configuration file.
@param fmt the formater to print on
- @param machine the main machine
**)
- let pp_project_configuration_file fmt machine =
+ let pp_project_configuration_file fmt =
fprintf fmt "pragma SPARK_Mode (On);"
(** Print the name of the ada project file.
@param base_name name of the lustre file
@param fmt the formater to print on
- @param machine_opt the main machine option
**)
- let pp_project_name basename fmt machine_opt =
+ let pp_project_name basename fmt =
fprintf fmt "%s.gpr" basename
let pp_for_single name arg fmt =
@@ -152,7 +150,7 @@ struct
pp_for_single "Library_Name" basename;
pp_for_single "Library_Dir" "lib";
]
- | Some machine -> [
+ | Some _ -> [
pp_for "Main" [asprintf "%t" pp_main_procedure_name];
pp_for_single "Exec_Dir" "bin";
])
diff --git a/src/backends/Ada/misc_lustre_function.ml b/src/backends/Ada/misc_lustre_function.ml
index 742d14e6f812d49426b0ccc8be46286ff71b497f..4e39f980615beb2527b86cc15242cbc84475d53b 100644
--- a/src/backends/Ada/misc_lustre_function.ml
+++ b/src/backends/Ada/misc_lustre_function.ml
@@ -79,7 +79,7 @@ let rec find_submachine_step_call ident instr_list =
(List.map (function x-> x.value_type) vl,
List.map (function x-> x.var_type) il)]
| MBranch (_, l) -> List.flatten
- (List.map (function x, y -> find_submachine_step_call ident y) l)
+ (List.map (function _, y -> find_submachine_step_call ident y) l)
| _ -> []
in
List.flatten (List.map search_instr instr_list)
@@ -155,7 +155,7 @@ let unification (substituion:(int*Types.type_expr) list) ((type_poly:Types.type_
@param calls a list of pair of list of types
@param return true if the two pairs are equal
**)
-let check_call_equal (i1, o1) (i2, o2) =
+let check_call_equal (i1, _) (i2, _) =
(List.for_all2 check_type_equal i1 i2)
&& (List.for_all2 check_type_equal i1 i2)
@@ -184,7 +184,7 @@ let get_substitution machine ident submachine =
let call = match calls with
(* assume that there is always one call to a subinstance *)
| [] -> assert(false)
- | h::t -> h in
+ | h::_ -> h in
(* assume that all the calls to a subinstance are using the same type *)
assert(check_calls call calls);
(* make a list of all types from input and output vars *)
@@ -235,7 +235,7 @@ let build_if g c1 i1 tl =
let neg = c1=tag_false in
let other = match tl with
| [] -> None
- | [(c2, i2)] -> Some i2
+ | [(_, i2)] -> Some i2
| _ -> assert false
in
match neg, other with
@@ -249,7 +249,7 @@ let rec push_if_in_expr = function
(
match get_instr_desc instr with
| MBranch (g, (c1, i1)::tl) when c1=tag_false || c1=tag_true ->
- let (neg, g, instrs1, instrs2) = build_if g c1 i1 tl in
+ let (_, g, instrs1, instrs2) = build_if g c1 i1 tl in
let instrs1_pushed = push_if_in_expr instrs1 in
let get_assign instr = match get_instr_desc instr with
| MLocalAssign (id, value) -> (false, id, value)
@@ -304,7 +304,7 @@ let rec push_if_in_expr = function
List.map get_assign instrs2_pushed
in
gen_assigns if_assigns else_assigns
- | x -> [instr]
+ | _ -> [instr]
)@(push_if_in_expr q)
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index c6849e832fc9caba0e80509018418069362cf205..21da76fe1d52b0b4a36f905ae9729aa69c6bce5b 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -83,13 +83,13 @@ let gen_files funs basename prog machines dependencies =
let source_mauve_out = open_out source_mauve_file in
let source_mauve_fmt = formatter_of_out_channel source_mauve_out in
(* Header *)
- print_mauve_header source_mauve_fmt m basename prog machines dependencies;
+ print_mauve_header source_mauve_fmt basename;
(* Shell *)
- print_mauve_shell source_mauve_fmt m basename prog machines dependencies;
+ print_mauve_shell source_mauve_fmt m;
(* Core *)
- print_mauve_core source_mauve_fmt m basename prog machines dependencies;
+ print_mauve_core source_mauve_fmt m;
(* FSM *)
- print_mauve_fsm source_mauve_fmt m basename prog machines dependencies;
+ print_mauve_fsm source_mauve_fmt m;
close_out source_mauve_out;
end
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 3254d8ebc60c52b527b2318fb3727fb730d0bbe4..d465ceee0bdca61abb6b56414421ffeda8e71e90 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -204,7 +204,7 @@ let pp_c_type ?(var_opt=None) var_id fmt t =
| Types.Tconst ty -> fprintf fmt "%s %s" ty var_id
| Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var_id
| _ -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
- in aux t (fun fmt () -> ())
+ in aux t (fun _ () -> ())
(*
let rec pp_c_initialize fmt t =
match (Types.repr t).Types.tdesc with
@@ -230,7 +230,7 @@ let rec pp_c_const fmt c =
(* | Const_float r -> pp_print_float fmt r *)
| Const_tag t -> pp_c_tag fmt t
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
- | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
+ | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_c_const fmt c)) fl
| Const_string _ | Const_modeid _ -> assert false (* string occurs in annotations not in C *)
@@ -244,7 +244,7 @@ let rec pp_c_val m self pp_var fmt v =
| Cst c -> pp_c_const fmt c
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " pp_c_val) vl
| Access (t, i) -> fprintf fmt "%a[%a]" pp_c_val t pp_c_val i
- | Power (v, n) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." (Machine_code_common.pp_val m) v; assert false)
+ | Power (v, _) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." (Machine_code_common.pp_val m) v; assert false)
| Var v ->
if Machine_code_common.is_memory m v then (
(* array memory vars are represented by an indirection to a local var with the right type,
@@ -342,7 +342,7 @@ let pp_c_decl_struct_var fmt id =
then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
else pp_c_type id.var_id fmt id.var_type
-let pp_c_decl_instance_var fmt (name, (node, static)) =
+let pp_c_decl_instance_var fmt (name, (node, _)) =
fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
let pp_c_checks self fmt m =
@@ -369,7 +369,7 @@ let pp_registers_struct fmt m =
else
()
-let print_machine_struct machines fmt m =
+let print_machine_struct fmt m =
if fst (Machine_code_common.get_stateless_status m) then
begin
end
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index cff0245a2f018ef5651fdc48b78f4ec1ad53c4de..1c0afa99ab4b9d39c37bef09b8960f325f612154 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -28,7 +28,7 @@ end
module EmptyMod =
struct
- let print_machine_decl_prefix = fun fmt x -> ()
+ let print_machine_decl_prefix = fun _ _ -> ()
end
module Main = functor (Mod: MODIFIERS_HDR) ->
@@ -120,7 +120,7 @@ let print_static_link_instance fmt (i, (m, _)) =
(* Allocation of a node struct:
- if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct)
*)
-let print_static_link_macro fmt (m, attr, inst) =
+let print_static_link_macro fmt (m, _, inst) =
let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
pp_machine_static_link_name m.mname.node_id
@@ -166,7 +166,7 @@ we do multiple things:
- if the node is a regular node associated to a contract, print the contract as function contract.
- do not print anything if this is a contract node
*)
-let print_machine_alloc_decl machines fmt m =
+let print_machine_alloc_decl fmt m =
Mod.print_machine_decl_prefix fmt m;
if fst (get_stateless_status m) then
begin
@@ -339,7 +339,7 @@ let print_header header_fmt basename prog machines dependencies =
pp_print_newline header_fmt ()
end
*)
-let print_alloc_header header_fmt basename prog machines dependencies spec =
+let print_alloc_header header_fmt basename _prog machines dependencies spec =
(* Include once: start *)
let baseNAME = file_to_module_name basename in
begin
@@ -358,12 +358,12 @@ let print_alloc_header header_fmt basename prog machines dependencies spec =
fprintf header_fmt "@]@.";
(* Print the struct definitions of all machines. *)
fprintf header_fmt "/* Struct definitions */@.";
- List.iter (print_machine_struct machines header_fmt) machines;
+ List.iter (print_machine_struct header_fmt) machines;
pp_print_newline header_fmt ();
fprintf header_fmt "/* Specification */@.%a@." C_backend_spec.pp_acsl_preamble spec;
(* Print the prototypes of all machines *)
fprintf header_fmt "/* Node allocation function/macro prototypes */@.";
- List.iter (print_machine_alloc_decl machines header_fmt) machines;
+ List.iter (print_machine_alloc_decl header_fmt) machines;
pp_print_newline header_fmt ();
(* Include once: end *)
fprintf header_fmt "#endif@.";
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 2dd1c9d500712fa0aa40f1bc90336cced5978b93..040c68c4d5c5514005d2cc30e3ffe6df941e606e 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -11,7 +11,6 @@
open Lustre_types
open Machine_code_types
-open Corelang
open Machine_code_common
open Format
open C_backend_common
@@ -206,7 +205,7 @@ let print_main_header fmt =
fprintf fmt (if !Options.cpp then "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.hpp\"@." else "#include <stdio.h>@.#include <unistd.h>@.#include <string.h>@.#include \"%s/io_frontend.h\"@.")
(Options_management.core_dependency "io_frontend")
-let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) =
+let print_main_c main_fmt main_machine basename _prog _machines _dependencies =
print_main_header main_fmt;
fprintf main_fmt "#include <stdlib.h>@.#include <assert.h>@.";
print_import_alloc_prototype main_fmt {local=true; name=basename; content=[]; is_stateful=true} (* assuming it is stateful*) ;
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index fc55185ba584aa7fbcf6395292d01dda0d8307c8..6dd4678a7a86a6fab2c67faf7202312d48e7d399 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -11,7 +11,6 @@
open Format
open Lustre_types
-open Corelang
let pp_dep fmt dep =
Format.fprintf fmt "%b, %s, {%a}, %b"
diff --git a/src/backends/C/c_backend_mauve.ml b/src/backends/C/c_backend_mauve.ml
index 5456f01e53884f106bd150cb385191d2224d78c4..d64a4af8f17b4a8975114fed4a744f3c76f0d673 100644
--- a/src/backends/C/c_backend_mauve.ml
+++ b/src/backends/C/c_backend_mauve.ml
@@ -1,7 +1,5 @@
open Lustre_types
open Machine_code_types
-open Corelang
-open Machine_code
open Format
open C_backend_common
open Utils
@@ -31,7 +29,7 @@ let fsm_name node = node ^ "FSM"
(* Hearder *)
(* -------------------------------------------------- *)
-let print_mauve_header fmt mauve_machine basename prog machines _ (*dependencies*) =
+let print_mauve_header fmt basename =
fprintf fmt "#include \"mauve/runtime.hpp\"@.";
print_import_alloc_prototype fmt {local=true; name=basename; content=[]; is_stateful=true} (* assuming it is stateful*) ;
pp_print_newline fmt ();
@@ -65,7 +63,7 @@ let print_mauve_default fmt mauve_machine v =
if not !found then fprintf fmt "%s" (mauve_default_value v)
-let print_mauve_shell fmt mauve_machine basename prog machines _ (*dependencies*) =
+let print_mauve_shell fmt mauve_machine =
let node_name = mauve_machine.mname.node_id in
fprintf fmt "/*@.";
@@ -116,7 +114,7 @@ let print_mauve_step fmt node_name mauve_machine =
(* Core *)
(* -------------------------------------------------- *)
-let print_mauve_core fmt mauve_machine basename prog machines _ (*dependencies*) =
+let print_mauve_core fmt mauve_machine =
let node_name = mauve_machine.mname.node_id in
fprintf fmt "/*@.";
@@ -196,7 +194,7 @@ let print_mauve_period fmt mauve_machine =
if not !found then fprintf fmt "0"
-let print_mauve_fsm fmt mauve_machine basename prog machines _ (*dependencies*) =
+let print_mauve_fsm fmt mauve_machine =
let node_name = mauve_machine.mname.node_id in
fprintf fmt "/*@.";
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 3e499b54316957dfe8acbeabce7f5edc60ead3aa..fb37f9b8c52d6d228674087b8057b36fcabbee41 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -11,9 +11,6 @@
open Format
open Lustre_types
-open Machine_code
-open C_backend_common
-open Utils
(**************************************************************************)
(* Printing spec for c *)
@@ -131,7 +128,7 @@ let print_machine_decl_prefix fmt m =
(* TODO ACSL
mspec are function body annotations, sush as loop invariants, acsl asserts ... *)
-let pp_mspec fmt s = ()
+let pp_mspec _ _ = ()
(* TODO ACSL
Return updates machines (eg with local annotations) and acsl preamble *)
@@ -145,7 +142,7 @@ let pp_acsl_preamble fmt preamble =
(* MAKEFILE *)
(**************************************************************************)
-let makefile_targets fmt basename nodename dependencies =
+let makefile_targets fmt basename _nodename dependencies =
fprintf fmt "FRAMACEACSL=`frama-c -print-share-path`/e-acsl@.";
(* EACSL version of library file . c *)
fprintf fmt "%s_eacsl.c: %s.c %s.h@." basename basename basename;
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 6929a66e9108f44dbc630150dbcc3cdae2fc7b47..9a26ef3ff4a35ae6a02a4ef04cdfbf691218c4ef 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -41,8 +41,8 @@ struct
| Var _ -> 0
| Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
| Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
- | Access (v, i) -> max 0 (expansion_depth v - 1)
- | Power (v, n) -> 0 (*1 + expansion_depth v*)
+ | Access (v, _) -> max 0 (expansion_depth v - 1)
+ | Power _ -> 0 (*1 + expansion_depth v*)
and expansion_depth_cst c =
match c with
Const_array cl -> 1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
@@ -61,8 +61,8 @@ struct
| Var _ -> []
| Fun (_, vl) -> List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
| Array vl -> true :: List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
- | Access (v, i) -> (match (static_loop_profile v) with [] -> [] | _ :: q -> q)
- | Power (v, n) -> false :: static_loop_profile v
+ | Access (v, _) -> (match (static_loop_profile v) with [] -> [] | _ :: q -> q)
+ | Power (v, _) -> false :: static_loop_profile v
and static_loop_profile_cst cst =
match cst with
Const_array cl -> List.fold_right
@@ -107,12 +107,12 @@ let rec mk_loop_variables m ty depth =
let reorder_loop_variables loop_vars =
let (int_loops, var_loops) =
- List.partition (function (d, LInt _) -> true | _ -> false) loop_vars
+ List.partition (function (_, LInt _) -> true | _ -> false) loop_vars
in
var_loops @ int_loops
(* Prints a one loop variable suffix for arrays *)
-let pp_loop_var m pp_val fmt lv =
+let pp_loop_var _ pp_val fmt lv =
match snd lv with
| LVar v -> fprintf fmt "[%s]" v
| LInt r -> fprintf fmt "[%d]" !r
@@ -160,7 +160,7 @@ let rec pp_value_suffix m self var_type loop_vars pp_var fmt value =
| [] , Array vl ->
let var_type = Types.array_element_type var_type in
Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix m self var_type [] pp_var)) vl
- | _ :: q, Power (v, n) ->
+ | _ :: q, Power (v, _) ->
pp_value_suffix m self var_type q pp_var fmt v
| _ , Fun (n, vl) ->
pp_basic_lib_fun (Types.is_int_type value.value_type) n (pp_value_suffix m self var_type loop_vars pp_var) fmt vl
@@ -443,35 +443,35 @@ let print_dealloc_code fmt m =
(Utils.fprintf_list ~sep:"" print_dealloc_array) array_mem
(Utils.fprintf_list ~sep:"" print_dealloc_instance) m.minstances
-let print_stateless_init_code dependencies fmt m self =
- let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
- let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
- fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
- (print_init_prototype self) (m.mname.node_id, m.mstatic)
- (* array mems *)
- (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
- (Utils.pp_final_char_if_non_empty ";@," array_mems)
- (* memory initialization *)
- (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
- (Utils.pp_newline_if_non_empty m.mmemory)
- (* sub-machines initialization *)
- (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
- (Utils.pp_newline_if_non_empty m.minit)
-
-let print_stateless_clear_code dependencies fmt m self =
- let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
- let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
- fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
- (print_clear_prototype self) (m.mname.node_id, m.mstatic)
- (* array mems *)
- (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
- (Utils.pp_final_char_if_non_empty ";@," array_mems)
- (* memory clear *)
- (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
- (Utils.pp_newline_if_non_empty m.mmemory)
- (* sub-machines clear*)
- (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
- (Utils.pp_newline_if_non_empty m.minit)
+(* let print_stateless_init_code fmt m self =
+ * let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+ * let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+ * fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+ * (print_init_prototype self) (m.mname.node_id, m.mstatic)
+ * (\* array mems *\)
+ * (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+ * (Utils.pp_final_char_if_non_empty ";@," array_mems)
+ * (\* memory initialization *\)
+ * (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
+ * (Utils.pp_newline_if_non_empty m.mmemory)
+ * (\* sub-machines initialization *\)
+ * (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
+ * (Utils.pp_newline_if_non_empty m.minit)
+ *
+ * let print_stateless_clear_code fmt m self =
+ * let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
+ * let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+ * fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+ * (print_clear_prototype self) (m.mname.node_id, m.mstatic)
+ * (\* array mems *\)
+ * (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+ * (Utils.pp_final_char_if_non_empty ";@," array_mems)
+ * (\* memory clear *\)
+ * (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
+ * (Utils.pp_newline_if_non_empty m.mmemory)
+ * (\* sub-machines clear*\)
+ * (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
+ * (Utils.pp_newline_if_non_empty m.minit) *)
let print_stateless_code dependencies fmt m =
let self = "__ERROR__" in
@@ -528,7 +528,7 @@ let print_reset_code dependencies fmt m self =
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.minit
(Utils.pp_newline_if_non_empty m.minit)
-let print_init_code dependencies fmt m self =
+let print_init_code fmt m self =
let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
@@ -543,7 +543,7 @@ let print_init_code dependencies fmt m self =
(Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
(Utils.pp_newline_if_non_empty m.minit)
-let print_clear_code dependencies fmt m self =
+let print_clear_code fmt m self =
let minit = List.map (fun i -> match get_instr_desc i with MReset i -> i | _ -> assert false) m.minit in
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
@@ -669,9 +669,9 @@ let print_machine dependencies fmt m =
if !Options.mpfr then
begin
(* Init function *)
- print_init_code dependencies fmt m self;
+ print_init_code fmt m self;
(* Clear function *)
- print_clear_code dependencies fmt m self;
+ print_clear_code fmt m self;
end
end
@@ -735,7 +735,7 @@ let print_lib_c source_fmt basename prog machines dependencies =
(* Print the struct definitions of all machines. *)
fprintf source_fmt "/* Struct definitions */@.";
fprintf source_fmt "@[<v>";
- List.iter (print_machine_struct machines source_fmt) machines;
+ List.iter (print_machine_struct source_fmt) machines;
fprintf source_fmt "@]@.";
pp_print_newline source_fmt ();
(* Print nodes one by one (in the previous order) *)
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index ab13ffc88ba5b57020304ce06588259454621e61..234ab9b780937c44518691405e0de7dc1e93230b 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -118,7 +118,7 @@ let fprintf_list = Utils.fprintf_list
-> false *)
let is_arrow_fun m i =
match Corelang.get_instr_desc i with
- | MStep ([var], i, vl) ->
+ | MStep ([_], i, vl) ->
(
try
let name = (get_node_def i m).node_id in
@@ -166,7 +166,7 @@ let get_instr_id fmt i =
match Corelang.get_instr_desc i with
| MLocalAssign(lhs,_) | MStateAssign (lhs, _) -> pp_var_name fmt lhs
| MReset i | MNoReset i -> fprintf fmt "%s" (reset_name i)
- | MBranch (g, _) -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
+ | MBranch _ -> incr branch_cpt; fprintf fmt "branch_%i" !branch_cpt
| MStep (outs, id, _) ->
print_protect fmt
(fun fmt -> fprintf fmt "%a_%s" (fprintf_list ~sep:"_" pp_var_name) outs id)
@@ -260,7 +260,7 @@ let merge_branches instrs =
in
let sorting_branches b1 b2 =
match Corelang.get_instr_desc b1, Corelang.get_instr_desc b2 with
- | MBranch(g1, hl1), MBranch(g2, hl) ->
+ | MBranch(g1, _), MBranch(g2, _) ->
compare g1 g2
| _ -> assert false
in
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index 2a451dbed787ebe60c0aad0f041ea6308e367c86..38bcb5bebc4418eb9b927a6a92d0cbcf702bdcc9 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -13,7 +13,7 @@ let rec get_idx x l =
let rec get_expr_vars v =
match v.value_desc with
- | Cst c -> VSet.empty
+ | Cst _ -> VSet.empty
| Var v -> VSet.singleton v
| Fun (_, args) -> List.fold_left (fun accu v -> VSet.union accu (get_expr_vars v)) VSet.empty args
| _ -> assert false (* Invalid argument *)
diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml
index e4bbd81473d910331458267456dfbaeb33f1c7ff..a615cd4da0f1b90cba8cbe344ec90b060d301f85 100644
--- a/src/backends/Horn/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -40,10 +40,10 @@ if !Options.main_node <> "" then
let machine = get_machine machines node in
if !Options.horn_cex then(
cex_computation machines fmt node machine;
- get_cex machines fmt node machine)
+ get_cex machines fmt machine)
else (
collecting_semantics machines fmt node machine;
- check_prop machines fmt node machine;
+ check_prop machines fmt machine;
)
end
@@ -100,7 +100,7 @@ let check_sfunction mannot =
begin
match x.annots with
[] -> false
- |[(key,va)] ->
+ |[(key, _)] ->
begin
match key with
[] -> false
@@ -119,7 +119,7 @@ let preprocess machines =
m :: res
) machines []
-let translate fmt basename prog machines=
+let translate fmt prog machines=
let machines = preprocess machines in
(* We print typedef *)
print_dep fmt prog; (*print static library e.g. math*)
diff --git a/src/backends/Horn/horn_backend_collecting_sem.ml b/src/backends/Horn/horn_backend_collecting_sem.ml
index 88fdeac7b6660df2915e7f9717e141657376fd7b..a69848fa4cbf04b861e624e72cdfcc541d86bd8e 100644
--- a/src/backends/Horn/horn_backend_collecting_sem.ml
+++ b/src/backends/Horn/horn_backend_collecting_sem.ml
@@ -17,7 +17,6 @@
open Format
open Lustre_types
-open Corelang
open Machine_code_types
open Horn_backend_common
@@ -102,7 +101,7 @@ let collecting_semantics machines fmt node machine =
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next
-let check_prop machines fmt node machine =
+let check_prop machines fmt machine =
let main_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
@@ -179,7 +178,7 @@ let cex_computation machines fmt node machine =
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine)
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) cex_memory_next
-let get_cex machines fmt node machine =
+let get_cex machines fmt machine =
let cex_input =
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
in
diff --git a/src/backends/Horn/horn_backend_common.ml b/src/backends/Horn/horn_backend_common.ml
index dc166cd5593979c1905c9c74d559a76ac73e3fa3..d7e1f12603eda04ea964797489a59894781d4780 100644
--- a/src/backends/Horn/horn_backend_common.ml
+++ b/src/backends/Horn/horn_backend_common.ml
@@ -30,8 +30,8 @@ let rec pp_type fmt t =
match (Types.repr t).Types.tdesc with
| Types.Tconst ty -> pp_print_string fmt ty
| Types.Tclock t -> pp_type fmt t
- | Types.Tarray(dim,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
- | Types.Tstatic(d, ty)-> pp_type fmt ty
+ | Types.Tarray(_,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
+ | Types.Tstatic(_, ty) -> pp_type fmt ty
| Types.Tarrow _
| _ -> eprintf "internal error: pp_type %a@."
Types.print_ty t; assert false
@@ -81,7 +81,7 @@ let rename_next = rename (fun n -> n ^ "_x")
let rename_next_list = List.map rename_next
-let local_memory_vars machines machine =
+let local_memory_vars machine =
rename_machine_list machine.mname.node_id machine.mmemory
let instances_memory_vars ?(without_arrow=false) machines machine =
@@ -126,20 +126,20 @@ let arrow_vars machines machine : Lustre_types.var_decl list =
aux true machine.mname.node_id machine
let full_memory_vars ?(without_arrow=false) machines machine =
- (local_memory_vars machines machine)
+ (local_memory_vars machine)
@ (instances_memory_vars ~without_arrow machines machine)
-let inout_vars machines m =
+let inout_vars m =
(rename_machine_list m.mname.node_id m.mstep.step_inputs)
@ (rename_machine_list m.mname.node_id m.mstep.step_outputs)
let step_vars machines m =
- (inout_vars machines m)
+ (inout_vars m)
@ (rename_current_list (full_memory_vars machines m))
@ (rename_next_list (full_memory_vars machines m))
let step_vars_m_x machines m =
- (inout_vars machines m)
+ (inout_vars m)
@ (rename_mid_list (full_memory_vars machines m))
@ (rename_next_list (full_memory_vars machines m))
@@ -148,7 +148,7 @@ let reset_vars machines m =
@ (rename_mid_list (full_memory_vars machines m))
let step_vars_c_m_x machines m =
- (inout_vars machines m)
+ (inout_vars m)
@ (rename_current_list (full_memory_vars machines m))
@ (rename_mid_list (full_memory_vars machines m))
@ (rename_next_list (full_memory_vars machines m))
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index f10a9fd1ca62ce23add4e9ae3c8336b57f6e1f6d..9576a3b946b280cbe0c503dc3d4b755ee1ac3e5e 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -27,7 +27,7 @@ open Horn_backend_common
(* Instruction Printing functions *)
(********************************************************************************************)
-let pp_horn_var m fmt id =
+let pp_horn_var _ fmt id =
(*if Types.is_array_type id.var_type
then
assert false (* no arrays in Horn output *)
@@ -39,7 +39,7 @@ let pp_horn_tag fmt t =
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
(* Prints a constant value *)
-let rec pp_horn_const fmt c =
+let pp_horn_const fmt c =
match c with
| Const_int i -> pp_print_int fmt i
| Const_real r -> Real.pp fmt r
@@ -56,13 +56,13 @@ let rec pp_default_val fmt t =
if Types.is_int_type t then fprintf fmt "0" else
if Types.is_real_type t then fprintf fmt "0" else
match (Types.dynamic_type t).Types.tdesc with
- | Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
+ | Types.Tarray _ -> (* TODO PL: this strange code has to be (heavily) checked *)
let valt = Types.array_element_type t in
fprintf fmt "((as const (Array Int %a)) %a)"
pp_type valt
pp_default_val valt
- | Types.Tstruct(l) -> assert false
- | Types.Ttuple(l) -> assert false
+ | Types.Tstruct _ -> assert false
+ | Types.Ttuple _ -> assert false
|_ -> assert false
let pp_mod pp_val v1 v2 fmt =
@@ -153,7 +153,7 @@ let rec pp_horn_val ?(is_lhs=false) m self pp_var fmt v =
(* Code specific for arrays *)
- | Power (v, n) -> assert false
+ | Power _ -> assert false
| Var v ->
if is_memory m v then
if Types.is_array_type v.var_type
@@ -267,7 +267,7 @@ let pp_instance_call machines reset_instances m fmt i inputs outputs =
fprintf fmt ")@]"
end
- | node_name_n -> begin
+ | _ -> begin
fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
pp_machine_step_name (node_name n)
(Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) inputs
@@ -311,7 +311,7 @@ let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ide
m (pp_horn_var m) fmt
(mk_val (Var i) i.var_type) v;
reset_instances
- | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
+ | MStep ([_], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
assert false (* This should not happen anymore *)
| MStep (il, i, vl) ->
(* if reset instance, just print the call over mem_m , otherwise declare mem_m =
@@ -366,7 +366,7 @@ and pp_machine_instrs machines reset_instances m fmt instrs =
| [] -> fprintf fmt "true"; reset_instances
let pp_machine_reset machines fmt m =
- let locals = local_memory_vars machines m in
+ let locals = local_memory_vars m in
fprintf fmt "@[<v 5>(and @ ";
(* print "x_m = x_c" for each local memory *)
@@ -418,7 +418,7 @@ let print_machine machines fmt m =
(* Printing variables *)
Utils.fprintf_list ~sep:"@." pp_decl_var fmt
(
- (inout_vars machines m)@
+ (inout_vars m)@
(rename_current_list (full_memory_vars machines m)) @
(rename_mid_list (full_memory_vars machines m)) @
(rename_next_list (full_memory_vars machines m)) @
@@ -432,7 +432,7 @@ let print_machine machines fmt m =
fprintf fmt "(declare-rel %a (%a))@."
pp_machine_stateless_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_type)
- (List.map (fun v -> v.var_type) (inout_vars machines m));
+ (List.map (fun v -> v.var_type) (inout_vars m));
match m.mstep.step_asserts with
| [] ->
@@ -444,7 +444,7 @@ let print_machine machines fmt m =
ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs);
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
pp_machine_stateless_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
+ (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars m);
end
| assertsl ->
begin
@@ -518,7 +518,7 @@ let mk_flags arity =
if i > arity then [] else i :: (range (i+1) j) in
range 2 arity;
in
- List.fold_left (fun acc x -> acc ^ " false") "true" b_range
+ List.fold_left (fun acc _ -> acc ^ " false") "true" b_range
(*Get sfunction infos from command line*)
@@ -555,7 +555,7 @@ let get_sf_info() =
((step_vars machines m)@
(rename_machine_list m.mname.node_id m.mstep.step_locals));
Format.pp_print_newline fmt ();
- let sf_name, flags, arity = get_sf_info() in
+ let sf_name, flags, _ = get_sf_info() in
if is_stateless m then
begin
@@ -579,7 +579,7 @@ let get_sf_info() =
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_reset_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_type)
- (List.map (fun v -> v.var_type) (inout_vars machines m));
+ (List.map (fun v -> v.var_type) (inout_vars m));
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_step_name m.mname.node_id
diff --git a/src/backends/Horn/horn_backend_traces.ml b/src/backends/Horn/horn_backend_traces.ml
index 99811029d26d52e08ff7d6769e7f12aefc6c3eb8..a9838824f8a5c6e680110bb6a15a3d99c0c51904 100644
--- a/src/backends/Horn/horn_backend_traces.ml
+++ b/src/backends/Horn/horn_backend_traces.ml
@@ -158,7 +158,7 @@ let pp_prefix_rev fmt prefix =
(List.rev prefix)
-let traces_file fmt basename prog machines =
+let traces_file fmt machines =
fprintf fmt "<?xml version=\"1.0\"?>@.";
fprintf fmt "<Traces xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">@.";
fprintf fmt "@[<v 5>@ %a@ @]@."
@@ -195,13 +195,13 @@ let traces_file fmt basename prog machines =
(Utils.fprintf_list ~sep:" | " pp_var) init_local_vars
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) init_local_vars
(fun fmt -> match memories_next with [] -> () | _ -> fprintf fmt "")
- (Utils.fprintf_list ~sep:" | " (fun fmt (prefix, ee) -> fprintf fmt "%a" pp_xml_expr ee)) memories_next;
+ (Utils.fprintf_list ~sep:" | " (fun fmt (_, ee) -> fprintf fmt "%a" pp_xml_expr ee)) memories_next;
fprintf fmt "<localStep name=\"%a\" type=\"%a\">%t%a</localStep>@ "
(Utils.fprintf_list ~sep:" | " pp_var) step_local_vars
(Utils.fprintf_list ~sep:" | " (fun fmt id -> pp_type fmt id.var_type)) step_local_vars
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt "")
- (Utils.fprintf_list ~sep:" | " (fun fmt (prefix,ee) -> fprintf fmt "(%a)"
+ (Utils.fprintf_list ~sep:" | " (fun fmt (_,ee) -> fprintf fmt "(%a)"
pp_xml_expr ee)) (memories_old);
let arrow_vars = arrow_vars machines m in
diff --git a/src/basic_library.ml b/src/basic_library.ml
index ad648d8d2a5d7ff5235f3c25079041ebef20839d..4317eaf5ad309aa200330bab0598ae8ac4d1ebfd 100644
--- a/src/basic_library.ml
+++ b/src/basic_library.ml
@@ -160,7 +160,7 @@ let is_stateless_fun x =
(* | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *)
(* | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false) *)
-let rec partial_eval op e opt =
+let partial_eval op e opt =
let open Lustre_types in
let is_zero e =
match e.expr_desc with
@@ -279,8 +279,8 @@ let rec partial_eval op e opt =
e.expr_desc
| "-", [e0; e] when is_zero e0 ->
Expr_appl("uminus", e, None)
- | ("*"|"/"), [e0; e] when is_zero e0 -> e0.expr_desc
- | "*", [e; e0] when is_zero e0 -> e0.expr_desc
+ | ("*"|"/"), [e0; _] when is_zero e0 -> e0.expr_desc
+ | "*", [_; e0] when is_zero e0 -> e0.expr_desc
| "*", [e1; e] when is_one e1 -> e.expr_desc
| "/", [e; e1] when is_one e1 -> e.expr_desc
| "&&", [efalse; _] when is_false efalse ->
diff --git a/src/causality.ml b/src/causality.ml
index a1fe1fe24e1ec45cade51c53332e3473199eb036..e480fe22859e50b6c4c7e560e18627b176ffe3ed 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -17,7 +17,6 @@
open Utils
open Lustre_types
open Corelang
-open Graph
type identified_call = eq * tag
@@ -682,7 +681,7 @@ module VarClockDep =
struct
let rec get_clock_dep ck =
match ck.Clocks.cdesc with
- | Clocks.Con (ck ,c ,l) -> l::(get_clock_dep ck)
+ | Clocks.Con (ck , _ ,l) -> l::(get_clock_dep ck)
| Clocks.Clink ck'
| Clocks.Ccarrying (_, ck') -> get_clock_dep ck'
| _ -> []
diff --git a/src/checks/access.ml b/src/checks/access.ml
index b24ab610071d2b7a967b25464355a77b5ff32741..604e5c45171e1b7ec39ccdddcf9a2427c4638a46 100644
--- a/src/checks/access.ml
+++ b/src/checks/access.ml
@@ -11,7 +11,7 @@
(** Access checking module. Done after typing. Generates dimension constraints stored in nodes *)
-let debug fmt args = () (* Format.eprintf "%a" *)
+let debug _fmt _args = () (* Format.eprintf "%a" *)
(* Though it shares similarities with the clock calculus module, no code
is shared. Simple environments, very limited identifier scoping, no
identifier redefinition allowed. *)
@@ -21,8 +21,6 @@ open Utils
overwritten, yet this makes notations far lighter.*)
open Lustre_types
open Corelang
-open Types
-open Format
module ConstraintModule =
struct (* bool dimension module *)
@@ -59,7 +57,7 @@ let rec check_expr checks expr =
| Expr_pre e1
| Expr_when (e1,_,_) -> check_expr checks e1
- | Expr_merge (_,hl) -> List.fold_left (fun checks (l, h) -> check_expr checks h) checks hl
+ | Expr_merge (_,hl) -> List.fold_left (fun checks (_, h) -> check_expr checks h) checks hl
in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res
let rec check_var_decl_type loc checks ty =
diff --git a/src/checks/algebraicLoop.ml b/src/checks/algebraicLoop.ml
index 215e8282073a7af2c560da2697898026f551c0f3..f3b3359ba3fe8fc1bffeb69040325c79e1ee8c20 100644
--- a/src/checks/algebraicLoop.ml
+++ b/src/checks/algebraicLoop.ml
@@ -73,11 +73,11 @@ end
let pp_resolution fmt resolution =
- fprintf_list ~sep:"@ " (fun fmt (eq, tag) ->
+ fprintf_list ~sep:"@ " (fun fmt (eq, _) ->
Format.fprintf fmt "inlining: %a" Printers.pp_node_eq eq
) fmt resolution
-let al_is_solved (_, als) = List.for_all (fun (vars, calls, status) -> status) als
+let al_is_solved (_, als) = List.for_all (fun (_, _, status) -> status) als
(**********************************************************************)
(* Functions to access or toggle the local inlining feature of a call *)
@@ -172,10 +172,10 @@ let fast_stages_processing prog =
let rec solving_node max_inlines prog nd existing_al partitions =
(* let pp_calls = pp_calls nd in *)
(* For each partition, we identify the original one *)
- let rerun, max_inlines, al = List.fold_left (fun (rerun, inlines, al) part ->
+ let rerun, max_inlines, al = List.fold_left (fun (rerun, _, _) part ->
let part_vars = ISet.of_list part in
(* Useful functions to filter list of elements *)
- let match_al (vars, calls, status) =
+ let match_al (vars, _, _) =
not (ISet.is_empty (ISet.inter (ISet.of_list vars) part_vars)) in
(* Identifying previous alarms that could be associated to current conflict *)
let matched, non_matched = List.partition match_al existing_al in
@@ -187,7 +187,7 @@ let rec solving_node max_inlines prog nd existing_al partitions =
hope so! *)
assert false
in
- let match_previous (eq, expr, fun_id) =
+ let match_previous (_, expr, _) =
List.exists
(fun (_, expr', _) -> expr'.expr_tag = expr.expr_tag)
previous_calls
@@ -216,7 +216,7 @@ let rec solving_node max_inlines prog nd existing_al partitions =
List.partition (fun (_, expr, _) -> is_expr_inlined nd expr) calls in
(* Inlining the first uninlined call *)
match possible_resolution with
- | (fun_id, expr, eq)::_ -> ((* One could inline expr *)
+ | (fun_id, expr, _)::_ -> ((* One could inline expr *)
Log.report ~level:2 (fun fmt-> Format.fprintf fmt "inlining call to %s@ " fun_id);
(* Forcing the expr to be inlined *)
let _ = inline_expr nd expr in
@@ -227,7 +227,7 @@ let rec solving_node max_inlines prog nd existing_al partitions =
max_inlines - 1,
(
part,
- List.map (fun ((eq, expr2, fcn_name) as call)-> call, (expr2.expr_tag = expr.expr_tag)) calls,
+ List.map (fun ((_, expr2, _) as call)-> call, (expr2.expr_tag = expr.expr_tag)) calls,
true (* TODO was false. Should be put it true and expect a final
scheduling to change it to false in case of failure ? *) (*
Status is nok, LA is unsolved yet *)
@@ -239,7 +239,7 @@ let rec solving_node max_inlines prog nd existing_al partitions =
max_inlines,
(
part, (* initial list of troublesogme variables *)
- List.map (fun ((eq, expr, fcn_name) as call) -> call, false) calls,
+ List.map (fun call -> call, false) calls,
false (* Status is nok, LA is unsolved *)
)::non_matched
@@ -308,14 +308,14 @@ let clean_al prog : program_t * bool * report =
(* (ident list * (ident * expr* bool) list * bool) *)
-let pp_al nd fmt (partition, calls, status) =
+let pp_al nd fmt (partition, calls, _) =
let open Format in
fprintf fmt "@[<v 0>";
fprintf fmt "variables in the alg. loop: @[<hov 0>%a@]@ "
(fprintf_list ~sep:",@ " pp_print_string) partition;
fprintf fmt "@ involved node calls: @[<v 0>%a@]@ "
(fprintf_list ~sep:",@ "
- (fun fmt ((funid, expr, eq), status) ->
+ (fun fmt ((funid, expr, _), status) ->
fprintf fmt "%s" funid;
if status && is_expr_inlined nd expr then fprintf fmt " (inlining it solves the alg. loop)";
)
@@ -335,7 +335,7 @@ let pp_al nd fmt (partition, calls, status) =
let pp_report fmt report =
let open Format in
fprintf_list ~sep:"@."
- (fun fmt (nd, als) ->
+ (fun _ (nd, als) ->
let top = Corelang.node_from_name (nd.node_id) in
let pp =
if not !Options.solve_al || List.exists (fun (_,_,valid) -> not valid) als then
diff --git a/src/checks/stateless.ml b/src/checks/stateless.ml
index 450bd316ca097f1f0c17447b04aa3c7656ae440b..4fee77e713288aea47563495805fd519e8e47ac1 100644
--- a/src/checks/stateless.ml
+++ b/src/checks/stateless.ml
@@ -31,8 +31,8 @@ let rec check_expr expr =
| Expr_arrow _
| Expr_fby _
| Expr_pre _ -> false
- | Expr_when (e', i, l)-> check_expr e'
- | Expr_merge (i, hl) -> List.for_all (fun (t, h) -> check_expr h) hl
+ | Expr_when (e', _, _)-> check_expr e'
+ | Expr_merge (_, hl) -> List.for_all (fun (_, h) -> check_expr h) hl
| Expr_appl (i, e', i') ->
let reset_opt = (match i' with None -> true | Some e'' -> check_expr e'') in
let stateless_node =
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 2324b49630c501e03c1aa040a58a3dcf3f93f7d8..c3175b38b56502363ed9a6897311fbc6580c5842 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -22,7 +22,6 @@ open Utils
open Lustre_types
open Corelang
open Clocks
-open Format
let loc_of_cond loc_containing id =
let pos_start =
@@ -151,7 +150,7 @@ let rec update_scope scoped ck =
update_scope scoped ck1; update_scope scoped ck2
| Ctuple clist ->
List.iter (update_scope scoped) clist
- | Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
+ | Con (ck', _, _) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
| Cvar | Cunivar -> ()
| Clink ck' ->
update_scope scoped ck'
@@ -519,7 +518,7 @@ and clock_carrier env c loc ce =
and clock_expr ?(nocarrier=true) env expr =
let resulting_ck =
match expr.expr_desc with
- | Expr_const cst ->
+ | Expr_const _ ->
let ck = new_var true in
expr.expr_clock <- ck;
ck
@@ -537,12 +536,12 @@ and clock_expr ?(nocarrier=true) env expr =
let ck = clock_standard_args env elist in
expr.expr_clock <- ck;
ck
- | Expr_access (e1, d) ->
+ | Expr_access (e1, _) ->
(* dimension, being a static value, doesn't need to be clocked *)
let ck = clock_standard_args env [e1] in
expr.expr_clock <- ck;
ck
- | Expr_power (e1, d) ->
+ | Expr_power (e1, _) ->
(* dimension, being a static value, doesn't need to be clocked *)
let ck = clock_standard_args env [e1] in
expr.expr_clock <- ck;
@@ -682,7 +681,7 @@ let clock_node env loc nd =
let new_env = clock_var_decl_list env false nd.node_inputs in
let new_env = clock_var_decl_list new_env true nd.node_outputs in
let new_env = clock_var_decl_list new_env true nd.node_locals in
- let eqs, auts = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.
+ let eqs, _ = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.
For the moment, it is ignored *)
List.iter (clock_eq new_env) eqs;
let ck_ins = clock_of_vlist nd.node_inputs in
diff --git a/src/clocks.ml b/src/clocks.ml
index 29892a36bf30bd665e9592f4be7f8a1757ed0fb2..aa37d0ba031a455bf6ede055d032903902953efa 100644
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -124,12 +124,12 @@ let new_carrier_name () =
let rec repr =
function
- {cdesc=Clink ck'} ->
+ {cdesc=Clink ck'; _} ->
repr ck'
| ck -> ck
let rec carrier_repr =
- function {carrier_desc = Carry_link cr'} -> carrier_repr cr'
+ function {carrier_desc = Carry_link cr'; _} -> carrier_repr cr'
| cr -> cr
@@ -217,7 +217,7 @@ let rec is_polymorphic ck =
(** [constrained_vars_of_clock ck] returns the clock variables subject
to sub-typing constraints appearing in clock [ck]. Removes duplicates *)
(* Used mainly for debug, non-linear complexity. *)
-let rec constrained_vars_of_clock ck =
+let constrained_vars_of_clock ck =
let rec aux vars ck =
match ck.cdesc with
| Cvar -> vars
@@ -253,12 +253,12 @@ let rec root ck =
| Carrow _ | Ctuple _ -> failwith "Internal error root"
(* Returns the branch of clock [ck] in its clock tree *)
-let rec branch ck =
+let branch ck =
let rec branch ck acc =
match (repr ck).cdesc with
| Ccarrying (_, ck) -> branch ck acc
| Con (ck, cr, l) -> branch ck ((cr, l) :: acc)
- | Ctuple (ck::_) -> branch ck acc
+ | Ctuple (ck::_) -> branch ck acc
| Ctuple _
| Carrow _ -> assert false
| _ -> acc
@@ -365,7 +365,7 @@ let rec print_ck_suffix fmt ck =
fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
| Clink ck' ->
print_ck_suffix fmt ck'
- | Ccarrying (cr,ck') ->
+ | Ccarrying (_, ck') ->
fprintf fmt "%a" print_ck_suffix ck'
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 05a7d1633c27cf61000895b02928fac88851d386..021772cbc39697995a1f71838c596e5a62e9b100 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -157,7 +157,7 @@ let check_top_decls header =
-let check_compatibility (prog, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
+let check_compatibility (_, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
try
(* checking defined types are compatible with declared types*)
Typing.check_typedef_compat header;
@@ -342,9 +342,9 @@ let resolve_contracts prog =
| Node nd -> (
match nd.node_spec with
| None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
- | Some (NodeSpec id) -> (* shall not happen, its too early *)
+ | Some (NodeSpec _) -> (* shall not happen, its too early *)
assert false
- | Some (Contract c) -> (* A contract: processing it *)
+ | Some (Contract _) -> (* A contract: processing it *)
(* we bind a fresh node *)
let new_nd = process_contract_new_node accu_contracts prog top in
(* Format.eprintf "Creating new contract node %s@." (node_name new_nd); *)
@@ -357,9 +357,9 @@ let resolve_contracts prog =
| ImportedNode ind -> ( (* Similar treatment for imported nodes *)
match ind.nodei_spec with
None -> accu_contracts, top::accu_nodes (* A boring node: no contract *)
- | Some (NodeSpec id) -> (* shall not happen, its too early *)
+ | Some (NodeSpec _) -> (* shall not happen, its too early *)
assert false
- | Some (Contract c) -> (* A contract: processing it *)
+ | Some (Contract _) -> (* A contract: processing it *)
(* we bind a fresh node *)
let new_nd = process_contract_new_node accu_contracts prog top in
let ind = { ind with nodei_spec = (Some (NodeSpec (node_name new_nd))) } in
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index d1efba16f3fc56805186e0bfd8b691c492d424a8..31f341234d437efcef3d49d6c16a6c9e5807a599 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -1,5 +1,4 @@
open Format
-open Utils
open Compiler_common
open Lustre_types
module Mpfr = Lustrec_mpfr
@@ -98,10 +97,10 @@ let stage1 params prog dirname basename extension =
in
(* Perform inlining before any analysis *)
- let orig, prog =
+ let _, prog =
if !Options.global_inline && !Global.main_node <> "" then
(if !Options.witnesses then prog else []),
- Inliner.global_inline basename prog
+ Inliner.global_inline prog
else (* if !Option.has_local_inline *)
[],
Inliner.local_inline prog (* type_env clock_env *)
@@ -306,7 +305,7 @@ let stage3 prog machine_code dependencies basename extension =
begin
Log.report ~level:1 (fun fmt -> fprintf fmt ".. Ada code generation@.");
Ada_backend.translate_to_ada
- basename prog (Machine_code_common.arrow_machine::machine_code) dependencies
+ basename (Machine_code_common.arrow_machine::machine_code)
end
| "horn", _ ->
begin
@@ -315,14 +314,14 @@ let stage3 prog machine_code dependencies basename extension =
let source_out = open_out source_file in
let fmt = formatter_of_out_channel source_out in
Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
- Horn_backend.translate fmt basename prog (Machine_code_common.arrow_machine::machine_code);
+ Horn_backend.translate fmt prog (Machine_code_common.arrow_machine::machine_code);
(* Tracability file if option is activated *)
if !Options.traces then (
let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
let traces_out = open_out traces_file in
let fmt = formatter_of_out_channel traces_out in
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
- Horn_backend_traces.traces_file fmt basename prog machine_code;
+ Horn_backend_traces.traces_file fmt machine_code;
)
end
| "lustre", _ ->
diff --git a/src/corelang.ml b/src/corelang.ml
index 0e8930c8c2827e641bbedfad6e959313b8556354..d2d9508787870e10c1f39f895680fe0bfe7e88bc 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -192,12 +192,14 @@ let mk_contract_var id is_const type_opt expr loc =
let v = mkvar_decl loc (id, typ, mkclock loc Ckdec_any, is_const, None, None) in
let eq = mkeq loc ([id], expr) in
{ empty_contract with locals = [v]; stmts = [Eq eq]; spec_loc = loc; }
-let eexpr_add_name eexpr name =
- {eexpr with eexpr_name = match name with "" -> None | _ -> Some name}
-let mk_contract_guarantees ?(name="") eexpr =
+
+let eexpr_add_name eexpr eexpr_name =
+ { eexpr with eexpr_name }
+
+let mk_contract_guarantees name eexpr =
{ empty_contract with guarantees = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
-let mk_contract_assume ?(name="") eexpr =
+let mk_contract_assume name eexpr =
{ empty_contract with assume = [eexpr_add_name eexpr name]; spec_loc = eexpr.eexpr_loc }
let mk_contract_mode id rl el loc =
@@ -255,7 +257,7 @@ let update_expr_annot node_id e annot =
e
-let mkinstr ?lustre_expr ?lustre_eq i =
+let mkinstr ?lustre_eq i =
{
instr_desc = i;
(* lustre_expr = lustre_expr; *)
@@ -318,8 +320,8 @@ let update_node id top =
let is_imported_node td =
match td.top_decl_desc with
- | Node nd -> false
- | ImportedNode nd -> true
+ | Node _ -> false
+ | ImportedNode _ -> true
| _ -> assert false
let is_node_contract nd =
@@ -582,7 +584,7 @@ let sort_handlers hl =
let rec is_eq_const c1 c2 =
match c1, c2 with
- | Const_real r1, Const_real r2
+ | Const_real r1, Const_real _
-> Real.eq r1 r1
| Const_struct lcl1, Const_struct lcl2
-> List.length lcl1 = List.length lcl2
@@ -650,7 +652,7 @@ let get_node_eqs =
end)
let get_node_eq id node =
- let eqs, auts = get_node_eqs node in
+ let eqs, _ = get_node_eqs node in
try
List.find (fun eq -> List.mem id eq.eq_lhs) eqs
with
@@ -757,7 +759,7 @@ let rec rename_static rename cty =
| Tydec_struct fl -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
| _ -> cty
-let rec rename_carrier rename cck =
+let rename_carrier rename cck =
match cck with
| Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
| _ -> cck
@@ -807,14 +809,14 @@ let rec rename_carrier rename cck =
| Expr_appl (i, e', i') ->
Expr_appl (f_node i, re e', Utils.option_map re i')
- let rename_var f_node f_var v = {
+ let rename_var f_var v = {
(copy_var_decl v) with
var_id = f_var v.var_id;
var_type = v.var_type;
var_clock = v.var_clock;
}
- let rename_vars f_node f_var = List.map (rename_var f_node f_var)
+ let rename_vars f_var = List.map (rename_var f_var)
let rec rename_eq f_node f_var eq = { eq with
eq_lhs = List.map f_var eq.eq_lhs;
@@ -828,7 +830,7 @@ let rec rename_carrier rename cck =
hand_until = List.map (
fun (l,e,b,id) -> l, rename_expr f_node f_var e, b, f_var id
) h.hand_until;
- hand_locals = rename_vars f_node f_var h.hand_locals;
+ hand_locals = rename_vars f_var h.hand_locals;
hand_stmts = rename_stmts f_node f_var h.hand_stmts;
hand_annots = rename_annots f_node f_var h.hand_annots;
@@ -853,7 +855,7 @@ and rename_eexpr f_node f_var ee =
{ ee with
eexpr_tag = Utils.new_tag ();
eexpr_qfexpr = rename_expr f_node f_var ee.eexpr_qfexpr;
- eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_node f_var vdecls) ee.eexpr_quantifiers;
+ eexpr_quantifiers = List.map (fun (typ,vdecls) -> typ, rename_vars f_var vdecls) ee.eexpr_quantifiers;
}
and rename_mode f_node f_var m =
let rename_ee = rename_eexpr f_node f_var in
@@ -879,7 +881,7 @@ and rename_mode f_node f_var m =
else
x
in
- let rename_var = rename_var f_node f_var in
+ let rename_var = rename_var f_var in
let rename_vars = List.map rename_var in
let rename_expr = rename_expr f_node f_var in
let rename_eexpr = rename_eexpr f_node f_var in
@@ -1104,7 +1106,7 @@ let rec substitute_expr vars_to_replace defs e =
}
- let rec expr_to_eexpr expr =
+ let expr_to_eexpr expr =
{ eexpr_tag = expr.expr_tag;
eexpr_qfexpr = expr;
eexpr_quantifiers = [];
@@ -1159,7 +1161,7 @@ let rec get_expr_calls nodes e =
| Expr_arrow (e1, e2)
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl
- | Expr_appl (i, e', i') ->
+ | Expr_appl (i, e', _) ->
if Basic_library.is_expr_internal_fun e then
(get_calls e')
else
@@ -1216,30 +1218,30 @@ let get_expr_vars e =
in
get_expr_vars Utils.ISet.empty e
-let rec expr_has_arrows e =
- expr_desc_has_arrows e.expr_desc
-and expr_desc_has_arrows expr_desc =
- match expr_desc with
- | Expr_const _
- | Expr_ident _ -> false
- | Expr_tuple el
- | Expr_array el -> List.exists expr_has_arrows el
- | Expr_pre e1
- | Expr_when (e1, _, _)
- | Expr_access (e1, _)
- | Expr_power (e1, _) -> expr_has_arrows e1
- | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
- | Expr_arrow (e1, e2)
- | Expr_fby (e1, e2) -> true
- | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
- | Expr_appl (i, e', i') -> expr_has_arrows e'
-
-and eq_has_arrows eq =
- expr_has_arrows eq.eq_rhs
-and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers
-and node_has_arrows node =
- let eqs, auts = get_node_eqs node in
- List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts
+(* let rec expr_has_arrows e =
+ * expr_desc_has_arrows e.expr_desc
+ * and expr_desc_has_arrows expr_desc =
+ * match expr_desc with
+ * | Expr_const _
+ * | Expr_ident _ -> false
+ * | Expr_tuple el
+ * | Expr_array el -> List.exists expr_has_arrows el
+ * | Expr_pre e1
+ * | Expr_when (e1, _, _)
+ * | Expr_access (e1, _)
+ * | Expr_power (e1, _) -> expr_has_arrows e1
+ * | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
+ * | Expr_arrow _
+ * | Expr_fby _ -> true
+ * | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
+ * | Expr_appl (_, e', _) -> expr_has_arrows e'
+ *
+ * and eq_has_arrows eq =
+ * expr_has_arrows eq.eq_rhs
+ * and aut_has_arrows aut = List.exists (fun h -> List.exists (fun stmt -> match stmt with Eq eq -> eq_has_arrows eq | Aut aut' -> aut_has_arrows aut') h.hand_stmts ) aut.aut_handlers
+ * and node_has_arrows node =
+ * let eqs, auts = get_node_eqs node in
+ * List.exists (fun eq -> eq_has_arrows eq) eqs || List.exists (fun aut -> aut_has_arrows aut) auts *)
@@ -1378,7 +1380,7 @@ let rec push_negations ?(neg=false) e =
mkpredef_call e.expr_loc "not" [e]
else
e
- | Expr_appl (op,_,_) ->
+ | Expr_appl _ ->
if neg then
mkpredef_call e.expr_loc "not" [e]
else
@@ -1428,7 +1430,7 @@ let rec partial_eval e =
let edesc =
match e.expr_desc with
| Expr_const _ -> e.expr_desc
- | Expr_ident id -> e.expr_desc
+ | Expr_ident _ -> e.expr_desc
| Expr_ite (g,t,e) -> (
let g, t, e = pa g, pa t, pa e in
match g.expr_desc with
diff --git a/src/corelang.mli b/src/corelang.mli
index 05519d9a44dedca216338ae0dff864da3a52949d..d42e19db93ed05d39dbf64c9f119e3b59dededf1 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -45,7 +45,7 @@ val mk_new_node_name: node_desc -> ident -> ident
val mktop: top_decl_desc -> top_decl
(* constructor for machine types *)
-val mkinstr: ?lustre_expr:expr -> ?lustre_eq: eq -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
+val mkinstr: (* ?lustre_expr:expr -> *)?lustre_eq: eq -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
val get_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc
val update_instr_desc: Machine_code_types.instr_t -> Machine_code_types.instr_t_desc -> Machine_code_types.instr_t
@@ -149,10 +149,13 @@ val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
(** val rename_expr f_node f_var expr *)
val rename_expr : (ident -> ident) -> (ident -> ident) -> expr -> expr
+
(** val rename_eq f_node f_var eq *)
val rename_eq : (ident -> ident) -> (ident -> ident) -> eq -> eq
+
(** val rename_aut f_node f_var aut *)
val rename_aut : (ident -> ident) -> (ident -> ident) -> automata_desc -> automata_desc
+
(** rename_prog f_node f_var f_const prog *)
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program_t -> program_t
val rename_node: (ident -> ident) -> (ident -> ident) -> node_desc -> node_desc
@@ -169,8 +172,8 @@ val copy_prog: top_decl list -> top_decl list
val mkeexpr: Location.t -> expr -> eexpr
val empty_contract: contract_desc
val mk_contract_var: ident -> bool -> type_dec option -> expr -> Location.t -> contract_desc
-val mk_contract_guarantees: ?name:string -> eexpr -> contract_desc
-val mk_contract_assume: ?name:string -> eexpr -> contract_desc
+val mk_contract_guarantees: string option -> eexpr -> contract_desc
+val mk_contract_assume: string option -> eexpr -> contract_desc
val mk_contract_mode: ident -> eexpr list -> eexpr list -> Location.t -> contract_desc
val mk_contract_import: ident -> expr -> expr -> Location.t -> contract_desc
val merge_contracts: contract_desc -> contract_desc -> contract_desc
@@ -189,7 +192,7 @@ val find_eq: ident list -> eq list -> eq * eq list
val get_expr_calls: top_decl list -> expr -> Utils.ISet.t
-val eq_has_arrows: eq -> bool
+(* val eq_has_arrows: eq -> bool *)
val push_negations: ?neg:bool -> expr -> expr
diff --git a/src/delay.ml b/src/delay.ml
index 306bce0940cad3049ada051192125a1cc6146ede..12c60525524d4504f434c09e58f983c493ba04c2 100644
--- a/src/delay.ml
+++ b/src/delay.ml
@@ -9,8 +9,8 @@
(* *)
(********************************************************************)
-(** Types definitions and a few utility functions on delay types. *)
-(** Delay analysis by type polymorphism instead of constraints *)
+(** Types definitions and a few utility functions on delay types.
+ Delay analysis by type polymorphism instead of constraints *)
open Utils
type delay_expr =
@@ -43,7 +43,7 @@ let new_univar () =
let rec repr =
function
- {ddesc = Dlink i'} ->
+ {ddesc = Dlink i'; _} ->
repr i'
| i -> i
diff --git a/src/dune b/src/dune
index 8690c7da4a1c90b15139ad3c03da4c9261922077..27cd125af017cebef40a022a8c4eb33e54d5da12 100644
--- a/src/dune
+++ b/src/dune
@@ -126,3 +126,44 @@
(public_name lustrev)
(modules main_lustre_verifier verifiers)
(libraries lustrec_lib verifier_register lustrec.scopes))
+
+(executable
+ (name main_lustre_importer)
+ (public_name lustrei)
+ (modules main_lustre_importer vhdl_deriving_yojson vhdl_json_lib)
+ (libraries yojson ppx_deriving_yojson.runtime)
+ (preprocess (pps ppx_deriving_yojson)))
+
+(library
+ (name tools_lib)
+ (package lustrec)
+ (wrapped false)
+ (modules basetypes datatype activeStates)
+ (libraries lustrec_lib))
+
+(executable
+ (name sf_sem)
+ (public_name lustresf)
+ (modules
+ sf_sem
+ model_simple
+ model_stopwatch
+ CPS_ccode_generator
+ CPS_transformer
+ CPS_interpreter
+ CPS_lustre_generator
+ CPS
+ theta
+ memo)
+ (libraries tools_lib))
+
+; (executable
+; (name main_parse_json_file)
+; (public_name json-parser)
+; (modules main_parse_json_file json_parser)
+; (libraries tools_lib cmdliner))
+
+; (executable
+; (name test_json_parser_variables)
+; (modules test_json_parser_variables json_parser)
+; (libraries tools_lib))
diff --git a/src/features/machine_types/machine_types.ml b/src/features/machine_types/machine_types.ml
index 982af131fc75fe540524a802bf9b1af827647690..bc7d3a3f7adef45ddcba239073771c16a00f5c0a 100644
--- a/src/features/machine_types/machine_types.ml
+++ b/src/features/machine_types/machine_types.ml
@@ -344,7 +344,7 @@ let register_var var typ =
(************** Registering annotations ******************)
-let register_node node_id vars annots =
+let register_node vars annots =
List.fold_left (fun accu annot ->
let annl = annot.annots in
List.fold_left (fun accu (kwd, value) ->
@@ -396,7 +396,7 @@ let load prog =
| Node nd ->
(* Format.eprintf "Registeing node %s@." nd.node_id; *)
let vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
- let constrained_vars = register_node nd.node_id vars nd.node_annot in
+ let constrained_vars = register_node vars nd.node_annot in
check_node nd constrained_vars;
(* Computing the node type *)
diff --git a/src/inliner.ml b/src/inliner.ml
index 8e4f2988b854c281638c9df8c8a7bf9caf46a225..1b8a90330c0495108537e71081ae1af5986fdd7b 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -19,7 +19,7 @@ let keyword = ["inlining"]
let is_inline_expr expr =
match expr.expr_annot with
| Some ann ->
- List.exists (fun (key, value) -> key = keyword) ann.annots
+ List.exists (fun (key, _) -> key = keyword) ann.annots
| None -> false
let check_node_name id = (fun t ->
@@ -106,6 +106,7 @@ the resulting expression is tuple_of_renamed_outputs
TODO: convert the specification/annotation/assert and inject them
*)
+
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
locals, eqs, asserts)
*)
@@ -118,9 +119,9 @@ let inline_call node loc uid args reset locals caller =
let eqs' = List.map (rename_eq (fun x -> x) rename) eqs in
let auts' = List.map (rename_aut (fun x -> x) rename) auts in
let input_arg_list = List.combine node.node_inputs (Corelang.expr_list_of_expr args) in
- let static_inputs, dynamic_inputs = List.partition (fun (vdecl, arg) -> vdecl.var_dec_const) input_arg_list in
+ let static_inputs, dynamic_inputs = List.partition (fun (vdecl, _) -> vdecl.var_dec_const) input_arg_list in
let static_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.dimension_of_expr arg) static_inputs in
- let carrier_inputs, other_inputs = List.partition (fun (vdecl, arg) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in
+ let carrier_inputs, _ = List.partition (fun (vdecl, _) -> Corelang.is_clock_dec_type vdecl.var_dec_type.ty_dec_desc) dynamic_inputs in
let carrier_inputs = List.map (fun (vdecl, arg) -> vdecl, Corelang.ident_of_expr arg) carrier_inputs in
let rename_static v =
try
@@ -330,7 +331,7 @@ let inline_all_calls node nodes =
-let witness filename main_name orig inlined type_env clock_env =
+let witness filename main_name orig inlined (* type_env clock_env *) =
let loc = Location.dummy_loc in
let rename_local_node nodes prefix id =
if List.exists (check_node_name id) nodes then
@@ -422,7 +423,7 @@ let witness filename main_name orig inlined type_env clock_env =
node_stateless = None;
node_spec = Some
(Contract
- (mk_contract_guarantees
+ (mk_contract_guarantees None
(mkeexpr loc (mkexpr loc (Expr_ident ok_ident)))
)
);
@@ -449,9 +450,9 @@ let witness filename main_name orig inlined type_env clock_env =
()
end (* xx *)
-let global_inline basename prog (*type_env clock_env*) =
+let global_inline prog (*type_env clock_env*) =
(* We select the main node desc *)
- let main_node, other_nodes, other_tops =
+ let main_node, other_nodes, _ =
List.fold_right
(fun top (main_opt, nodes, others) ->
match top.top_decl_desc with
diff --git a/src/lusic.ml b/src/lusic.ml
index a84171c4ecf81cce123bf4776d6b5e5980e22715..d8cf1676521c59d29f69a236565920bfea227f69 100644
--- a/src/lusic.ml
+++ b/src/lusic.ml
@@ -12,7 +12,6 @@
open Format
open Lustre_types
-open Corelang
(********************************************************************************************)
(* Lusic to/from Header Printing functions *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index e80233bf4ca6c3acd46bf5ff788e8b75b5264b50..cad30eeda363180c65e3684719429a22c340cdcf 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -136,7 +136,7 @@ let rec translate_expr env expr =
raise NormalizationError)
| Expr_when (e1, _, _) -> (translate_expr e1).value_desc
- | Expr_merge (x, _) -> raise NormalizationError
+ | Expr_merge _ -> raise NormalizationError
| Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
let nd = node_from_name id in
Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 4925452383f50f10ad6f1368e0e0ad36569d4475..28233c112f9ddcda71fd4aaf9269a46c87c4af7a 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -118,7 +118,7 @@ let pp_machines fmt ml =
let rec is_const_value v =
match v.value_desc with
| Cst _ -> true
- | Fun (id, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
+ | Fun (_, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
| _ -> false
(* Returns the declared stateless status and the computed one. *)
@@ -130,8 +130,8 @@ let get_stateless_status m =
let is_stateless m = m.minstances = [] && m.mmemory = []
-let is_input m id =
- List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs
+(* let is_input m id =
+ * List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
let is_output m id =
List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
@@ -336,7 +336,7 @@ and join_guards inst1 insts2 =
match get_instr_desc inst1, List.map get_instr_desc insts2 with
| _ , [] ->
[inst1]
- | MBranch (x1, hl1), MBranch (x2, hl2) :: q when x1 = x2 ->
+ | MBranch (x1, hl1), MBranch (x2, hl2) :: _ when x1 = x2 ->
mkinstr
(* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
(MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 0e7bc0feeca67d6fa1794d5f2cc175015f92e2e7..aa4d9ef56d02e7550e5214fee1e483f8f24a0a24 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -10,12 +10,10 @@
(********************************************************************)
open Format
-open Log
open Compiler_common
open Utils
-open Lustre_types
-
+
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
@@ -40,7 +38,7 @@ let print_lusi prog dirname basename extension =
(* compile a .lus source file *)
-let rec compile dirname basename extension =
+let compile dirname basename extension =
let source_name = dirname ^ "/" ^ basename ^ extension in
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index 95dccd2367cb189da4d2dec94ae22d60fb6ace31..2c4f73a423346a25ce05406415652456ed40abc2 100644
--- a/src/main_lustre_testgen.ml
+++ b/src/main_lustre_testgen.ml
@@ -15,7 +15,6 @@ open Format
open Log
open Utils
-open Lustre_types
open Compiler_common
let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
@@ -46,18 +45,18 @@ let testgen_source dirname basename extension =
(* Parsing source *)
let prog = parse source_name extension in
let params = Backends.get_normalization_params () in
- let prog, dependencies =
+ let prog, _ =
try
Compiler_stages.stage1 params prog dirname basename extension
- with Compiler_stages.StopPhase1 prog -> (
- if !Options.print_nodes then (
- Format.printf "%a@.@?" Printers.pp_node_list prog;
- exit 0
+ with Compiler_stages.StopPhase1 prog -> (
+ if !Options.print_nodes then (
+ Format.printf "%a@.@?" Printers.pp_node_list prog;
+ exit 0
+ )
+ else
+ assert false
)
- else
- assert false
- )
- in
+ in
(* Two cases
- generation of coverage conditions
diff --git a/src/main_lustre_verifier.ml b/src/main_lustre_verifier.ml
index 7aed1884f27a985d2028b0c8950228c6f954fc08..da8d9de1b1f94c0b07ef3d17b04b6f9444b6b2f8 100644
--- a/src/main_lustre_verifier.ml
+++ b/src/main_lustre_verifier.ml
@@ -10,12 +10,10 @@
(********************************************************************)
open Format
-open Log
open Compiler_common
open Utils
-open Lustre_types
-
+
let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m"
@@ -41,7 +39,7 @@ we have multiple "backends"
shall be provided with ranges for inputs or local variables (memories)
*)
-let rec verify dirname basename extension =
+let verify dirname basename extension =
let source_name = dirname ^ "/" ^ basename ^ extension in
Options.compile_header := false; (* to avoid producing .h / .lusic *)
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
@@ -58,7 +56,7 @@ let rec verify dirname basename extension =
decr Options.verbose_level;
let params = Verifier.get_normalization_params () in
(* Normalizing it *)
- let prog, dependencies =
+ let prog, _ =
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
try
incr Options.verbose_level;
@@ -101,7 +99,7 @@ let rec verify dirname basename extension =
(*assert (dependencies = []); (* Do not handle deps yet *)*)
incr Options.verbose_level;
- Verifier.run basename prog machine_code;
+ Verifier.run ~basename prog machine_code;
begin
decr Options.verbose_level;
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ ");
diff --git a/src/mmap.ml b/src/mmap.ml
index 7d65bc6bc93299c5b7bba60f2804667765aae61a..e744cd92c26c41bf05855c05d23117c29887400c 100644
--- a/src/mmap.ml
+++ b/src/mmap.ml
@@ -123,23 +123,23 @@ module Make(Ord: OrderedType) = struct
let rec mem x = function
Empty ->
false
- | Node(l, v, d, r, _) ->
+ | Node(l, v, _, r, _) ->
let c = Ord.compare x v in
c = 0 || mem x (if c < 0 then l else r)
let rec min_binding = function
Empty -> raise Not_found
- | Node(Empty, x, d, r, _) -> (x, d)
- | Node(l, x, d, r, _) -> min_binding l
+ | Node(Empty, x, d, _, _) -> (x, d)
+ | Node(l, _, _, _, _) -> min_binding l
let rec max_binding = function
Empty -> raise Not_found
- | Node(l, x, d, Empty, _) -> (x, d)
- | Node(l, x, d, r, _) -> max_binding r
+ | Node(_, x, d, Empty, _) -> (x, d)
+ | Node(_, _, _, r, _) -> max_binding r
let rec remove_min_binding = function
Empty -> invalid_arg "Map.remove_min_elt"
- | Node(Empty, x, d, r, _) -> r
+ | Node(Empty, _, _, r, _) -> r
| Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r
let merge t1 t2 =
@@ -153,7 +153,7 @@ module Make(Ord: OrderedType) = struct
let rec remove x = function
Empty ->
Empty
- | Node(l, v, d, r, h) ->
+ | Node(l, v, d, r, _) ->
let c = Ord.compare x v in
if c = 0 then
merge l r
@@ -209,12 +209,12 @@ module Make(Ord: OrderedType) = struct
let rec add_min_binding k v = function
| Empty -> singleton k v
- | Node (l, x, d, r, h) ->
+ | Node (l, x, d, r, _) ->
bal (add_min_binding k v l) x d r
let rec add_max_binding k v = function
| Empty -> singleton k v
- | Node (l, x, d, r, h) ->
+ | Node (l, x, d, r, _) ->
bal l x d (add_max_binding k v r)
(* Same as create and bal, but no assumptions are made on the
@@ -263,7 +263,7 @@ module Make(Ord: OrderedType) = struct
| (Node (l1, v1, d1, r1, h1), _) when h1 >= height s2 ->
let (l2, d2, r2) = split v1 s2 in
concat_or_join (merge f l1 l2) v1 (f v1 (Some d1) d2) (merge f r1 r2)
- | (_, Node (l2, v2, d2, r2, h2)) ->
+ | (_, Node (l2, v2, d2, r2, _)) ->
let (l1, d1, r1) = split v2 s1 in
concat_or_join (merge f l1 l2) v2 (f v2 d1 (Some d2)) (merge f r1 r2)
| _ ->
diff --git a/src/modules.ml b/src/modules.ml
index bb5b9f692363632f379b008c5560dedbd92fd406..157847f0862e9dfb731fcd934e2d40581585c1ef 100644
--- a/src/modules.ml
+++ b/src/modules.ml
@@ -21,15 +21,15 @@ let name_dependency loc (local, dep) ext =
raise (Error.Error (loc, Error.Unknown_library dep))
-let add_symbol loc msg hashtbl name value =
- if Hashtbl.mem hashtbl name
- then raise (Error.Error (loc, Error.Already_bound_symbol msg))
- else Hashtbl.add hashtbl name value
+(* let add_symbol loc msg hashtbl name value =
+ * if Hashtbl.mem hashtbl name
+ * then raise (Error.Error (loc, Error.Already_bound_symbol msg))
+ * else Hashtbl.add hashtbl name value *)
-let check_symbol loc msg hashtbl name =
- if not (Hashtbl.mem hashtbl name)
- then raise (Error.Error (loc, Error.Unbound_symbol msg))
- else ()
+(* let check_symbol loc msg hashtbl name =
+ * if not (Hashtbl.mem hashtbl name)
+ * then raise (Error.Error (loc, Error.Unbound_symbol msg))
+ * else () *)
let add_imported_node name value =
@@ -73,7 +73,7 @@ let add_field loc name typ =
raise (Error.Error (loc, Error.Already_bound_symbol ("struct field " ^ name)))
else Hashtbl.add field_table name typ
-let import_typedef name tydef =
+let import_typedef tydef =
let loc = tydef.top_decl_loc in
let rec import ty =
match ty with
@@ -86,11 +86,11 @@ let import_typedef name tydef =
if not (Hashtbl.mem type_table (Tydec_const c))
then raise (Error.Error (loc, Error.Unbound_symbol ("type " ^ c)))
else ()
- | Tydec_array (c, ty) -> import ty
+ | Tydec_array (_, ty) -> import ty
| _ -> ()
in import ((typedef_of_top tydef).tydef_desc)
-let add_type itf name value =
+let add_type _itf name value =
(*Format.eprintf "Modules.add_type %B %s %a (owner=%s)@." itf name Printers.pp_typedef (typedef_of_top value) value.top_decl_owner;*)
try
let value' = Hashtbl.find type_table (Tydec_const name) in
@@ -100,16 +100,16 @@ let add_type itf name value =
let itf = value.top_decl_itf in
match value'.top_decl_desc, value.top_decl_desc with
| TypeDef ty', TypeDef ty when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf' && (not itf) -> ()
- | TypeDef ty', TypeDef ty -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("type " ^ name)))
+ | TypeDef _, TypeDef _ -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("type " ^ name)))
| _ -> assert false
- with Not_found -> (import_typedef name value; Hashtbl.add type_table (Tydec_const name) value)
+ with Not_found -> (import_typedef value; Hashtbl.add type_table (Tydec_const name) value)
-let check_type loc name =
- if not (Hashtbl.mem type_table (Tydec_const name))
- then raise (Error.Error (loc, Error.Unbound_symbol ("type " ^ name)))
- else ()
+(* let check_type loc name =
+ * if not (Hashtbl.mem type_table (Tydec_const name))
+ * then raise (Error.Error (loc, Error.Unbound_symbol ("type " ^ name)))
+ * else () *)
-let add_const itf name value =
+let add_const name value =
try
let value' = Hashtbl.find consts_table name in
let owner' = value'.top_decl_owner in
@@ -118,7 +118,7 @@ let add_const itf name value =
let itf = value.top_decl_itf in
match value'.top_decl_desc, value.top_decl_desc with
| Const c', Const c when c.const_value = c'.const_value && owner' = owner && itf' && (not itf) -> ()
- | Const c', Const c -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("const " ^ name)))
+ | Const _, Const _ -> raise (Error.Error (value.top_decl_loc, Error.Already_bound_symbol ("const " ^ name)))
| _ -> assert false
with Not_found -> Hashtbl.add consts_table name value
@@ -165,8 +165,8 @@ let get_envs_from_const const_decl (ty_env, ck_env) =
(Env.add_value ty_env const_decl.const_id const_decl.const_type,
Env.add_value ck_env const_decl.const_id (Clocks.new_var true))
-let get_envs_from_consts const_decls (ty_env, ck_env) =
- List.fold_right get_envs_from_const const_decls (ty_env, ck_env)
+(* let get_envs_from_consts const_decls (ty_env, ck_env) =
+ * List.fold_right get_envs_from_const const_decls (ty_env, ck_env) *)
let rec get_envs_from_top_decl (ty_env, ck_env) top_decl =
match top_decl.top_decl_desc with
@@ -258,7 +258,7 @@ let get_envs_from_top_decls header =
LoadError ("imported node " ^ ind.nodei_id ^
" declared in a regular Lustre file")))
| Const c -> (
- add_const is_header c.const_id decl;
+ add_const c.const_id decl;
decl::accu_prog, accu_dep, typ_env', clk_env'
)
| TypeDef tdef -> (
@@ -281,7 +281,7 @@ let load ~is_header program =
in
List.rev prog, List.rev deps, (typ_env, clk_env)
with
- Error.Error (loc, err) as exc -> (
+ Error.Error (_, err) as exc -> (
(* Format.eprintf "Import error: %a%a@."
* Error.pp_error_msg err
* Location.pp_loc loc; *)
diff --git a/src/modules.mli b/src/modules.mli
index e9e5aaa54ca2861ca3bca2c3962d450b5c2a1068..0d4cc2fafaf5f31da13160e4b5476c47bb92c6b5 100644
--- a/src/modules.mli
+++ b/src/modules.mli
@@ -1,5 +1,4 @@
open Lustre_types
-open Utils
(* This module is used to load lusic files when open(ing) modules in
lustre/lusi sources *)
diff --git a/src/mutation.ml b/src/mutation.ml
index 4b19fca761a8735a37d9bf96eadcbca91aa887a4..a5bc43f661e9e9d56f8d5495c3e16ce84c8c2fb5 100644
--- a/src/mutation.ml
+++ b/src/mutation.ml
@@ -80,7 +80,7 @@ let merge_records records_list =
nb_boolexpr = r1.nb_boolexpr + r2.nb_boolexpr;
nb_pre = r1.nb_pre + r2.nb_pre;
- nb_op = OpCount.merge (fun op r1opt r2opt ->
+ nb_op = OpCount.merge (fun _ r1opt r2opt ->
match r1opt, r2opt with
| None, _ -> r2opt
| _, None -> r1opt
@@ -114,7 +114,7 @@ let rec compute_records_expr expr =
merge_records (
({empty_records with nb_pre = 1})
::[compute_records_expr e])
- | Expr_appl (op_id, args, r) ->
+ | Expr_appl (op_id, args, _) ->
if List.mem op_id ops then
merge_records (
({empty_records with nb_op = OpCount.singleton op_id 1})
@@ -255,7 +255,7 @@ let select_in_list list rdm_mutate_elem =
let rec rdm_mutate_expr expr =
let mk_e d = { expr with expr_desc = d } in
match expr.expr_desc with
- | Expr_ident id -> rdm_mutate_var expr
+ | Expr_ident _ -> rdm_mutate_var expr
| Expr_const c ->
let new_const = rdm_mutate_const_value c in
let mut = check_mut (mk_cst_expr c) (mk_cst_expr new_const) in
@@ -318,7 +318,7 @@ let rnd_mutate_stmt stmt =
Printers.pp_node_eq eq
Printers.pp_node_eq new_eq);
mut, Eq new_eq
- | Aut aut -> assert false
+ | Aut _ -> assert false
let rdm_mutate_node nd =
let mutation, new_node_stmts =
@@ -407,9 +407,9 @@ let print_directive_json fmt d =
| Pre _ -> Format.fprintf fmt "\"mutation\": \"pre\""
| Boolexpr _ -> Format.fprintf fmt "\"mutation\": \"not\""
| Op (o, _, d) -> Format.fprintf fmt "\"mutation\": \"op_conv\", \"from\": \"%s\", \"to\": \"%s\"" o d
- | IncrIntCst n -> Format.fprintf fmt "\"mutation\": \"cst_incr\""
- | DecrIntCst n -> Format.fprintf fmt "\"mutation\": \"cst_decr\""
- | SwitchIntCst (n, m) -> Format.fprintf fmt "\"mutation\": \"cst_switch\", \"to_cst\": \"%i\"" m
+ | IncrIntCst _ -> Format.fprintf fmt "\"mutation\": \"cst_incr\""
+ | DecrIntCst _ -> Format.fprintf fmt "\"mutation\": \"cst_decr\""
+ | SwitchIntCst (_, m) -> Format.fprintf fmt "\"mutation\": \"cst_switch\", \"to_cst\": \"%i\"" m
let print_loc_json fmt (n,eqlhs, l) =
Format.fprintf fmt "\"node_id\": \"%s\", \"eq_lhs\": [%a], \"loc_line\": \"%i\""
@@ -526,7 +526,7 @@ let rec fold_mutate_expr expr =
current_loc := Some expr.expr_loc;
let new_expr =
match expr.expr_desc with
- | Expr_ident id -> fold_mutate_var expr
+ | Expr_ident _ -> fold_mutate_var expr
| _ -> (
let new_desc = match expr.expr_desc with
| Expr_const c -> Expr_const (fold_mutate_const_value c)
@@ -563,7 +563,7 @@ let fold_mutate_eq eq =
let fold_mutate_stmt stmt =
match stmt with
| Eq eq -> Eq (fold_mutate_eq eq)
- | Aut aut -> assert false
+ | Aut _ -> assert false
let fold_mutate_node nd =
@@ -740,7 +740,7 @@ let fold_mutate nb prog =
in
let find_next_new mutants mutant =
- let rec find_next_new init current =
+ let find_next_new init current =
if init = current || List.mem current mutants then raise Not_found else
(* TODO: check if we can generate more cases. The following lines were
diff --git a/src/normalization.ml b/src/normalization.ml
index d3611b39b5b7ff74a99b6cd2402a5da161daab40..f23a66fb21fc242f02f4d7ad518562e1cab5d41b 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -144,7 +144,7 @@ let mk_expr_alias_opt opt norm_ctx (defs, vars) expr =
Log.report ~plugin:"normalization" ~level:2
(fun fmt -> Format.fprintf fmt "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock);
match expr.expr_desc with
- | Expr_ident alias ->
+ | Expr_ident _ ->
(defs, vars), expr
| _ ->
match get_expr_alias defs expr with
@@ -223,7 +223,7 @@ let mk_norm_expr offsets ref_e norm_d =
expr_type = Utils.repeat (List.length offsets) drop_array_type ref_e.expr_type }
(* normalize_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
-let rec normalize_list alias norm_ctx offsets norm_element defvars elist =
+let normalize_list alias norm_ctx offsets norm_element defvars elist =
List.fold_right
(fun t (defvars, qlist) ->
let defvars, norm_t = norm_element alias norm_ctx offsets defvars t in
@@ -244,7 +244,7 @@ let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defva
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
let norm_expr = mk_norm_expr offsets expr (Expr_power (norm_e1, d)) in
mk_expr_alias_opt alias norm_ctx defvars norm_expr
- | Expr_power (e1, d) ->
+ | Expr_power (e1, _) ->
normalize_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
| Expr_access (e1, d) ->
normalize_expr ~alias:alias norm_ctx (d::offsets) defvars e1
@@ -288,7 +288,7 @@ let rec normalize_expr ?(alias=true) ?(alias_basic=false) norm_ctx offsets defva
mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
|| not (Basic_library.is_expr_internal_fun expr)))
norm_ctx defvars norm_expr
- | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
+ | Expr_arrow _ when !params.unfold_arrow_active && not (is_expr_once expr) ->
(* Here we differ from Colaco paper: arrows are pushed to the top *)
normalize_expr ~alias:alias norm_ctx offsets defvars (unfold_arrow expr)
| Expr_arrow (e1,e2) ->
@@ -341,7 +341,7 @@ and normalize_array_expr ?(alias=true) norm_ctx offsets defvars expr =
| Expr_power (e1, d) when offsets = [] ->
let defvars, norm_e1 = normalize_expr norm_ctx offsets defvars e1 in
defvars, mk_norm_expr offsets expr (Expr_power (norm_e1, d))
- | Expr_power (e1, d) ->
+ | Expr_power (e1, _) ->
normalize_array_expr ~alias:alias norm_ctx (List.tl offsets) defvars e1
| Expr_access (e1, d) -> normalize_array_expr ~alias:alias norm_ctx (d::offsets) defvars e1
| Expr_array elist when offsets = [] ->
@@ -401,7 +401,7 @@ let decouple_outputs norm_ctx defvars eq =
(Clocks.clock_list_of_clock eq.eq_rhs.expr_clock) in
defvars', {eq with eq_lhs = lhs' }
-let rec normalize_eq norm_ctx defvars eq =
+let normalize_eq norm_ctx defvars eq =
(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
match eq.eq_rhs.expr_desc with
| Expr_pre _
@@ -446,7 +446,7 @@ let normalize_eq_split norm_ctx defvars eq =
(* Projecting an eexpr to an eexpr associated to a single
variable. Returns the updated ee, the bounded variable and the
associated statement *)
-let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
+let normalize_pred_eexpr norm_ctx (def,vars) ee =
assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
(* don't do anything is eexpr is just a variable *)
let skip =
@@ -584,7 +584,7 @@ let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
(* We use node local vars to make sure we are creating fresh variables *)
-let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
+let normalize_spec parentid (in_vars, out_vars, l_vars) s =
(* Original set of variables actually visible from here: in/out and
spec locals (no node locals) *)
let orig_vars = in_vars @ out_vars @ s.locals in
@@ -608,7 +608,7 @@ let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
let process_predicates l defvars =
(* Format.eprintf "ProcPred: vars: %a@." Printers.pp_vars (snd defvars); *)
let res = List.fold_right (fun ee (accu, defvars) ->
- let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
+ let ee', defvars = normalize_pred_eexpr norm_ctx defvars ee in
ee'::accu, defvars
) l ([], defvars)
in
@@ -669,7 +669,7 @@ let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =
- new equations
-
*)
-let normalize_node decls node =
+let normalize_node node =
reset_cpt_fresh ();
let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
let not_is_orig_var v =
@@ -695,7 +695,6 @@ let normalize_node decls node =
| Some (NodeSpec _) -> node.node_spec, [], eqs
| Some (Contract s) ->
let new_locals, new_stmts, s' = normalize_spec
- decls
node.node_id
(node.node_inputs, node.node_outputs, node.node_locals)
s
@@ -801,20 +800,20 @@ let normalize_node decls node =
node
)
-let normalize_inode decls nd =
+let normalize_inode nd =
reset_cpt_fresh ();
match nd.nodei_spec with
None | Some (NodeSpec _) -> nd
| Some (Contract _) -> assert false
-let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =
+let normalize_decl (decl: top_decl) : top_decl =
match decl.top_decl_desc with
| Node nd ->
- let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
+ let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
update_node nd.node_id decl';
decl'
| ImportedNode nd ->
- let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode decls nd)} in
+ let decl' = {decl with top_decl_desc = ImportedNode (normalize_inode nd)} in
update_node nd.nodei_id decl';
decl'
@@ -825,7 +824,7 @@ let normalize_prog p decls =
params := p;
(* Main algorithm: iterates over nodes *)
- List.map (normalize_decl decls) decls
+ List.map normalize_decl decls
(* Fake interface for outside uses *)
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 81eb797843941802dad5c37e8006284f29872d9a..d2267ee27507e302eb373e1e9269a9365f16b896 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -32,8 +32,8 @@ let rec eliminate m elim instr =
| MSpec _ | MComment _ -> instr
| MLocalAssign (i,v) -> update_instr_desc instr (MLocalAssign (i, e_expr v))
| MStateAssign (i,v) -> update_instr_desc instr (MStateAssign (i, e_expr v))
- | MReset i -> instr
- | MNoReset i -> instr
+ | MReset _ -> instr
+ | MNoReset _ -> instr
| MStep (il, i, vl) -> update_instr_desc instr (MStep(il, i, List.map e_expr vl))
| MBranch (g,hl) ->
update_instr_desc instr (
@@ -75,7 +75,7 @@ let unfold_expr_offset m offset expr =
List.fold_left
(fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
(Types.array_element_type res.value_type)
- | Field f -> Format.eprintf "internal error: not yet implemented !"; assert false))
+ | Field _ -> Format.eprintf "internal error: not yet implemented !"; assert false))
expr offset
let rec simplify_cst_expr m offset typ cst =
@@ -96,7 +96,7 @@ let rec simplify_cst_expr m offset typ cst =
let simplify_expr_offset m expr =
let rec simplify offset expr =
match offset, expr.value_desc with
- | Field f ::q , _ -> failwith "not yet implemented"
+ | Field _ ::_ , _ -> failwith "not yet implemented"
| _ , Fun (id, vl) when Basic_library.is_value_internal_fun expr
-> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
| _ , Fun _
@@ -116,8 +116,8 @@ let rec simplify_instr_offset m instr =
match get_instr_desc instr with
| MLocalAssign (v, expr) -> update_instr_desc instr (MLocalAssign (v, simplify_expr_offset m expr))
| MStateAssign (v, expr) -> update_instr_desc instr (MStateAssign (v, simplify_expr_offset m expr))
- | MReset id -> instr
- | MNoReset id -> instr
+ | MReset _ -> instr
+ | MNoReset _ -> instr
| MStep (outputs, id, inputs) -> update_instr_desc instr (MStep (outputs, id, List.map (simplify_expr_offset m) inputs))
| MBranch (cond, brl)
-> update_instr_desc instr (
@@ -158,12 +158,12 @@ let is_unfoldable_expr fanin expr =
| _ , Var _ -> true
| [] , Power _
| [] , Array _ -> false
- | Index i :: q, Power (v, _) -> unfold q v
+ | Index _ :: q, Power (v, _) -> unfold q v
| Index i :: q, Array vl when Dimension.is_dimension_const i
-> unfold q (List.nth vl (Dimension.size_const_dimension i))
| _ , Array _ -> false
| _ , Access (v, i) -> unfold (Index (dimension_of_value i) :: offset) v
- | _ , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
+ | _ , Fun (_, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
-> List.for_all (unfold offset) vl
| _ , Fun _ -> false
| _ -> assert false
@@ -180,7 +180,7 @@ let unfoldable_assign fanin v expr =
&& basic_unfoldable_assign fanin v expr
let merge_elim elim1 elim2 =
- let merge k e1 e2 =
+ let merge _ e1 e2 =
match e1, e2 with
| Some e1, Some e2 -> if e1 = e2 then Some e1 else None
| _ , Some e2 -> Some e2
@@ -442,7 +442,7 @@ let instrs_cse m subst instrs =
*)
let machine_cse subst machine =
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_cse %a@." pp_elim subst);*)
- let subst, instrs = instrs_cse machine subst machine.mstep.step_instrs in
+ let _, instrs = instrs_cse machine subst machine.mstep.step_instrs in
let assigned = assigns_instrs instrs VSet.empty
in
{
@@ -467,7 +467,7 @@ let rec instr_is_skip instr =
match get_instr_desc instr with
| MLocalAssign (i, { value_desc = (Var v) ; _}) when i = v -> true
| MStateAssign (i, { value_desc = Var v; _}) when i = v -> true
- | MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
+ | MBranch (_, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
| _ -> false
and instrs_are_skip instrs =
List.for_all instr_is_skip instrs
@@ -487,7 +487,7 @@ and instrs_remove_skip instrs cont =
let rec value_replace_var fvar value =
match value.value_desc with
- | Cst c -> value
+ | Cst _ -> value
| Var v -> { value with value_desc = Var (fvar v) }
| Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
| Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
@@ -499,8 +499,8 @@ let rec instr_replace_var fvar instr cont =
| MSpec _ | MComment _ -> instr_cons instr cont
| MLocalAssign (i, v) -> instr_cons (update_instr_desc instr (MLocalAssign (fvar i, value_replace_var fvar v))) cont
| MStateAssign (i, v) -> instr_cons (update_instr_desc instr (MStateAssign (i, value_replace_var fvar v))) cont
- | MReset i -> instr_cons instr cont
- | MNoReset i -> instr_cons instr cont
+ | MReset _ -> instr_cons instr cont
+ | MNoReset _ -> instr_cons instr cont
| MStep (il, i, vl) -> instr_cons (update_instr_desc instr (MStep (List.map fvar il, i, List.map (value_replace_var fvar) vl))) cont
| MBranch (g, hl) -> instr_cons (update_instr_desc instr (MBranch (value_replace_var fvar g, List.map (fun (h, il) -> (h, instrs_replace_var fvar il [])) hl))) cont
@@ -527,7 +527,7 @@ let step_replace_var fvar step =
step_instrs = instrs_replace_var fvar step.step_instrs [];
}
-let rec machine_replace_variables fvar m =
+let machine_replace_variables fvar m =
{ m with
mstep = step_replace_var fvar m.mstep
}
@@ -549,7 +549,7 @@ let rec instr_assign res instr =
match get_instr_desc instr with
| MLocalAssign (i, _) -> Disjunction.CISet.add i res
| MStateAssign (i, _) -> Disjunction.CISet.add i res
- | MBranch (g, hl) -> List.fold_left (fun res (h, b) -> instrs_assign res b) res hl
+ | MBranch (_, hl) -> List.fold_left (fun res (_, b) -> instrs_assign res b) res hl
| MStep (il, _, _) -> List.fold_right Disjunction.CISet.add il res
| _ -> res
@@ -560,7 +560,7 @@ let rec instr_constant_assign var instr =
match get_instr_desc instr with
| MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
| MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
- | MBranch (g, hl) -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl
+ | MBranch (_, hl) -> List.for_all (fun (_, b) -> instrs_constant_assign var b) hl
| _ -> false
and instrs_constant_assign var instrs =
@@ -584,7 +584,7 @@ let rec instrs_fusion instrs =
| [], []
| [_], [_] ->
instrs
- | i1::i2::q, i1_desc::(MBranch ({ value_desc = Var v; _}, hl))::q_desc when instr_constant_assign v i1 ->
+ | i1::_::q, _::(MBranch ({ value_desc = Var v; _}, hl))::_ when instr_constant_assign v i1 ->
instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
| i1::i2::q, _ ->
i1 :: instrs_fusion (i2::q)
@@ -595,7 +595,7 @@ let step_fusion step =
step_instrs = instrs_fusion step.step_instrs;
}
-let rec machine_fusion m =
+let machine_fusion m =
{ m with
mstep = step_fusion m.mstep
}
diff --git a/src/options_management.ml b/src/options_management.ml
index cfc14857b490cecc5ed3bf0e22c5e64c62d373d2..ac48093bebbb83caa69c1ae8ef0d9756938ae1ca 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -61,7 +61,7 @@ let search_lib_path (local, full_file_name) =
let core_dependency lib_name =
search_lib_path (false, lib_name ^ ".h")
-let name_dependency (local, dep) ext =
+let name_dependency (_, dep) ext =
let dir = search_lib_path (false, dep ^ ext) in
dir ^ "/" ^ dep
diff --git a/src/pathConditions.ml b/src/pathConditions.ml
index fea864096d9bc5cb14a7068c5802e8aa646da728..280adfde89374a71aa178cb3301aeb7a1139b200 100644
--- a/src/pathConditions.ml
+++ b/src/pathConditions.ml
@@ -1,7 +1,6 @@
open Lustre_types
open Corelang
open Log
-open Format
module IdSet = Set.Make (struct type t = expr * int let compare = compare end)
@@ -30,7 +29,7 @@ let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ]
fmt "pre "; print_pre fmt (nb_pre-1) )
*)
-let rec mk_pre n e =
+let mk_pre n e =
if n <= 0 then
e
else
@@ -141,7 +140,7 @@ let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) =
vl, List.map
(fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
- | Expr_appl (op_name, args, r) when List.mem op_name rel_op ->
+ | Expr_appl (op_name, _, _) when List.mem op_name rel_op ->
[], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
| Expr_appl (op_name, args, r) ->
@@ -205,7 +204,7 @@ let rec mcdc_expr cpt_pre expr =
| Expr_pre e ->
let vl = mcdc_expr (cpt_pre+1) e in
vl
- | Expr_appl (f, args, r) ->
+ | Expr_appl (_, args, _) ->
let vl = mcdc_expr cpt_pre args in
vl
| _ -> []
@@ -222,7 +221,7 @@ let mcdc_node_eq eq =
let vl =
match eq.eq_lhs, Types.is_bool_type eq.eq_rhs.expr_type, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
| [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs
- | _::_, false, Types.Ttuple tl, Expr_tuple rhs ->
+ | _::_, false, Types.Ttuple _, Expr_tuple rhs ->
(* We iterate trough pairs, but accumulate variables aside. The resulting
expression shall remain a tuple defintion *)
let vl = List.fold_right2 (fun lhs rhs accu ->
@@ -240,7 +239,7 @@ let mcdc_node_eq eq =
let mcdc_node_stmt stmt =
match stmt with
| Eq eq -> let vl = mcdc_node_eq eq in vl
- | Aut aut -> assert false
+ | Aut _ -> assert false
let mcdc_top_decl td =
match td.top_decl_desc with
diff --git a/src/plugins/mpfr/lustrec_mpfr.ml b/src/plugins/mpfr/lustrec_mpfr.ml
index 0f43e6d772e84b34753c6b0ea98b2271951f8908..cffcb0fd10c4575828f8cb7740adc658f410702a 100644
--- a/src/plugins/mpfr/lustrec_mpfr.ml
+++ b/src/plugins/mpfr/lustrec_mpfr.ml
@@ -68,7 +68,7 @@ let pp_inject_copy pp_var fmt var value =
pp_var value
(mpfr_rnd ())
-let rec pp_inject_assign pp_var fmt var value =
+let pp_inject_assign pp_var fmt var value =
if is_const_value value
then
pp_inject_real pp_var pp_var fmt var value
@@ -172,7 +172,7 @@ let expr_of_const_array expr =
| _ -> assert false
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
-let rec inject_list alias node inject_element defvars elist =
+let inject_list alias node inject_element defvars elist =
List.fold_right
(fun t (defvars, qlist) ->
let defvars, norm_t = inject_element alias node defvars t in
@@ -245,7 +245,7 @@ and inject_branches node defvars hl =
hl (defvars, [])
-let rec inject_eq node defvars eq =
+let inject_eq node defvars eq =
let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
let norm_eq = { eq with eq_rhs = norm_rhs } in
norm_eq::defs', vars'
@@ -283,7 +283,7 @@ let inject_node node =
if auts != [] then assert false; (* Automata should be expanded by now. *)
List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in
(* Normalize the asserts *)
- let vars, assert_defs, asserts =
+ let vars, assert_defs, _ =
List.fold_left (
fun (vars, def_accu, assert_accu) assert_ ->
let assert_expr = assert_.assert_expr in
diff --git a/src/plugins/pluginType.ml b/src/plugins/pluginType.ml
index 3c8c1e79c0b6c95c99de822a4a66ef308ade0f63..100b4ff21f14c6ec69d8a899250cceab13d8bf60 100644
--- a/src/plugins/pluginType.ml
+++ b/src/plugins/pluginType.ml
@@ -17,7 +17,7 @@ module Default =
let usage fmt = Format.fprintf fmt "No specific help."
let init () = ()
let check_force_stateful () = false
- let refine_machine_code prog machines = machines
- let c_backend_main_loop_body_prefix basename mname fmt () = ()
- let c_backend_main_loop_body_suffix fmt () = ()
+ let refine_machine_code _prog machines = machines
+ let c_backend_main_loop_body_prefix _basename _mname _fmt () = ()
+ let c_backend_main_loop_body_suffix _fmt () = ()
end
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index daa75f4c5157fd8236a79d6d159c67b02aa02e02..e6e961d3783dc795ea69a6b12b9f3f2ddd8b55d4 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -94,7 +94,7 @@ let rec get_path prog machines node id_list accu =
let instance =
List.find
(fun i -> match get_instr_desc i with
- | MStep(p, o, _) -> List.exists find_var p
+ | MStep(p, _, _) -> List.exists find_var p
| _ -> false
)
e_machine.mstep.step_instrs
@@ -186,13 +186,13 @@ let extract_scopes_defs scopes =
in
scopes_vars
-let pp_scopes_files basename mname fmt scopes =
+let pp_scopes_files _basename _mname fmt scopes =
let scopes_vars = extract_scopes_defs scopes in
List.iteri (fun idx _(*(id, (var_path, var))*) ->
C_backend_common.pp_file_decl fmt "out_scopes" idx)
scopes_vars;
Format.fprintf fmt "@[<v 2>if (traces) {@ ";
- List.iteri (fun idx (id, (var_path, var)) ->
+ List.iteri (fun idx (id, (_, var)) ->
let file = C_backend_common.pp_file_open fmt "out_scopes" idx in
Format.fprintf fmt
"fprintf(%s, \"# scope: %s\\n\");@ "
@@ -266,7 +266,7 @@ let rec is_valid_path path nodename prog machines =
(* ; *)
res
- | inst::nodename::path' -> (* We use the scopes computed on the prog artifact *)
+ | _::nodename::path' -> (* We use the scopes computed on the prog artifact *)
(* Format.eprintf "Path is %a@ Local scopes: @[<v>%a@ @]@." *)
(* (Utils.fprintf_list ~sep:"." Format.pp_print_string) path *)
(* (Utils.fprintf_list ~sep:";@ " *)
diff --git a/src/printers.ml b/src/printers.ml
index f94505884365ad6c6b81c0199f2239d44efd8799..b51161bae64be0803533688497d4166909f8a4c0 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -194,7 +194,7 @@ and pp_app fmt id e r =
)
| _ -> None, e
in
- let when_expr, unwhen_ed_e = un_when_ed_expr e in
+ let when_expr, _ = un_when_ed_expr e in
match r, when_expr with
| None, None -> pp_call fmt id e
| None, Some w ->
@@ -397,7 +397,7 @@ let pp_spec_eq fmt eq =
let pp_spec_stmt fmt stmt =
match stmt with
| Eq eq -> pp_spec_eq fmt eq
- | Aut aut -> assert false (* Not supported yet *)
+ | Aut _ -> assert false (* Not supported yet *)
let pp_spec fmt spec =
diff --git a/src/real.ml b/src/real.ml
index dce155355d19f0c2241d5eed5103a301e39a0204..218018b8a039064b56f5f81369e5da9ec73a9a5d 100644
--- a/src/real.ml
+++ b/src/real.ml
@@ -1,12 +1,12 @@
(* (a, b, c) means a * 10^-b. c is the original string *)
type t = Q.t * int * string
-let pp fmt (c, e, s) =
+let pp fmt (_, _, s) =
Format.fprintf fmt "%s%s"
s
(if String.get s (-1 + String.length s) = '.' then "0" else "")
-let pp_ada fmt (c, e, s) =
+let pp_ada fmt (c, e, _) =
Format.fprintf fmt "%s.0*1.0e-%i" (Q.to_string c) e
let create m e s = Q.of_string m, e, s
@@ -33,8 +33,8 @@ let to_num = to_q
let to_string (_, _, s) = s
-let eq r1 r2 =
- Q.equal (to_q r1) (to_q r2)
+(* let eq r1 r2 =
+ * Q.equal (to_q r1) (to_q r2) *)
let num_binop op r1 r2 =
diff --git a/src/real.mli b/src/real.mli
index 59d3fb0196c10910ebd0759aed33146b019134b1..5fe806b03dba5823825cf6efeb61dd42b40a4d8a 100644
--- a/src/real.mli
+++ b/src/real.mli
@@ -21,7 +21,7 @@ val diseq: t -> t -> bool
(*val to_num: t -> Num.num*)
val to_q: t -> Q.t
val to_string: t -> string
-val eq: t -> t -> bool
+(* val eq: t -> t -> bool *)
val zero: t
val is_zero: t -> bool
diff --git a/src/scheduling.ml b/src/scheduling.ml
index 1405eee5fb46d28aa1683c6f84b7dae4e7dd9e2b..a030269e83340de7facef97fa0bfd4844009016f 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -12,7 +12,6 @@
open Utils
open Lustre_types
open Corelang
-open Graph
open Causality
open Scheduling_type
diff --git a/src/sortProg.ml b/src/sortProg.ml
index ec22bace353b18e6c43a0de4fd692818e46d6f80..0b4d03f475bb9cc9ad8173b747fafda4eed5e188 100644
--- a/src/sortProg.ml
+++ b/src/sortProg.ml
@@ -10,7 +10,6 @@
(********************************************************************)
open Lustre_types
-open Corelang
open Utils
let get_node nid prog =
diff --git a/src/splitting.ml b/src/splitting.ml
index d7e37a13ec038c9db58bb9306f383a01300cde57..1a868c8ee35eb2c8333d692ea7c3875f546e358b 100644
--- a/src/splitting.ml
+++ b/src/splitting.ml
@@ -12,7 +12,6 @@
open Utils
open Corelang
open Lustre_types
-open Format
let rec tuple_split_expr expr =
@@ -70,7 +69,7 @@ let rec tuple_split_expr expr =
(fun hl -> {expr with expr_tag = Utils.new_tag (); expr_desc = Expr_merge (c, List.combine tl hl) })
(transpose_list hl)
-let rec tuple_split_eq eq =
+let tuple_split_eq eq =
let split_rhs = tuple_split_expr eq.eq_rhs in
if List.length split_rhs = 1
then
diff --git a/src/tools/importer/main_lustre_importer.ml b/src/tools/importer/main_lustre_importer.ml
index 50e144428db1cab1a523b541fa2926c2b23d5781..2037ed5d15b78c6ef99de4160962ef00ebb091cf 100644
--- a/src/tools/importer/main_lustre_importer.ml
+++ b/src/tools/importer/main_lustre_importer.ml
@@ -16,9 +16,8 @@ open Vhdl_test
open Yojson.Safe
open Vhdl_deriving_yojson
open Vhdl_json_lib
-open Printf
-let _ =
+let () =
(*
(* Load model with Yojson *)
let json = xx in
diff --git a/src/tools/importer/vhdl_json_lib.ml b/src/tools/importer/vhdl_json_lib.ml
index 0c2fee4f3c1fbad11b349ee70cb787beb2572352..50dc68b88bfe4386e75a9ee294071d98ae678fa1 100644
--- a/src/tools/importer/vhdl_json_lib.ml
+++ b/src/tools/importer/vhdl_json_lib.ml
@@ -1,4 +1,3 @@
-open Yojson.Safe
open Yojson.Safe.Util
let rec assoc_map_except_str l f str =
@@ -40,7 +39,7 @@ let rec name_pair_list_to_string l =
(name_pair_list_to_string tl)
| _ -> []
-let rec assoc_filter_string l str =
+let assoc_filter_string l =
match l with
| `Assoc (x) -> name_pair_list_to_string x
| _ -> []
@@ -59,12 +58,12 @@ let rec pairlist_remove str l f =
(******************)
let rec assoc_elem_fst pair_list =
match pair_list with
- | (t,j)::tl -> t::(assoc_elem_fst tl)
+ | (t, _)::tl -> t::(assoc_elem_fst tl)
| [] -> []
let rec assoc_elem_snd pair_list =
match pair_list with
- | (t,j)::tl -> j::(assoc_elem_snd tl)
+ | (_, j)::tl -> j::(assoc_elem_snd tl)
| [] -> []
let rec assoc_elem_filter pair_list str =
@@ -88,7 +87,7 @@ let rec assoc_elem_filter_snd pair_list str =
else assoc_elem_filter_snd tl str
| [] -> []
-let rec assoc_elem_filternot_snd pair_list str =
+let assoc_elem_filternot_snd pair_list str =
match pair_list with
| (t,j)::tl -> if (not (String.equal t str)) then
j::(assoc_elem_filter_snd tl str)
@@ -119,7 +118,7 @@ let vhdl_json_designunits_content_as_list json =
let designunits_contents = json |> member "DESIGN_FILE" |> all_members "DESIGN_UNIT" in
`List designunits_contents
-let vhdl_json_designfile_content_excluding json str =
+let vhdl_json_designfile_content_excluding json =
json |> member "DESIGN_FILE" |> retain_other_members "DESIGN_UNIT"
let vhdl_json_list_designunits json =
@@ -128,7 +127,7 @@ let vhdl_json_list_designunits json =
let rec pairlist_contains_str str l =
match l with
- | (t,j)::tl -> if (String.equal t str) then true else pairlist_contains_str str tl
+ | (t, _)::tl -> if (String.equal t str) then true else pairlist_contains_str str tl
| [] -> false
(*
@@ -187,8 +186,8 @@ let rec to_list_content_str str json =
let rec prune_null_assoc json =
match json with
- | `Assoc ((t, `Assoc([]))::tl) -> prune_null_assoc (`Assoc tl)
- | `Assoc ((t, `Null)::tl) -> prune_null_assoc (`Assoc tl)
+ | `Assoc ((_, `Assoc([]))::tl) -> prune_null_assoc (`Assoc tl)
+ | `Assoc ((_, `Null)::tl) -> prune_null_assoc (`Assoc tl)
| `Assoc ((t, j)::tl) -> `Assoc ((t, (prune_null_assoc j))::(map_snd prune_null_assoc tl))
| `List (`Null::[]) -> `Null
| `List (l) -> `List (List.map prune_null_assoc l)
diff --git a/src/tools/seal/seal_export.ml b/src/tools/seal/seal_export.ml
index 8c750487d248355c3edc2973e2479bf3ba1da212..5715478dd33be7a137ffced018688dd8a094a1a9 100644
--- a/src/tools/seal/seal_export.ml
+++ b/src/tools/seal/seal_export.ml
@@ -81,7 +81,7 @@ let sw_to_lustre m sw_init sw_step init_out update_out =
| [] -> [] (* the system is stateless. Returning an empty list
shall do the job *)
- | (gl, up)::_ ->
+ | (_, up)::_ ->
List.map (fun (v,_) -> v) up
in
let loc = Location.dummy_loc in
diff --git a/src/tools/seal/seal_extract.ml b/src/tools/seal/seal_extract.ml
index f0e99518474e2ada14957522b193ddeac8df98ee..1a03b411140ed500de81a8eb2efebd055cb88248 100644
--- a/src/tools/seal/seal_extract.ml
+++ b/src/tools/seal/seal_extract.ml
@@ -53,12 +53,12 @@ let mem_expr e =
let mem_zexpr ze =
Hashtbl.mem ze_hash ze
let get_zexpr e =
- let eref, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
+ let _, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in
(* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)
Hashtbl.find e_hash uid
let get_expr ze =
let uid = Hashtbl.find ze_hash ze in
- let e,_ = List.find (fun (e,t) -> t = uid) !expr_hash in
+ let e,_ = List.find (fun (_, t) -> t = uid) !expr_hash in
e
let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e
@@ -317,7 +317,7 @@ let implies =
true
| _ -> if !seal_debug then report ~level:6 (fun fmt -> Format.fprintf fmt "not proved valid@ ");
false
- with Zustre_common.UnknownFunction(id, msg) -> (
+ with Zustre_common.UnknownFunction(_, msg) -> (
report ~level:1 msg;
false
)
@@ -411,7 +411,7 @@ let check_sat ?(just_check=false) (l: elem_boolexpr guard) : bool * (elem_boolex
)
)
- with Zustre_common.UnknownFunction(id, msg) -> (
+ with Zustre_common.UnknownFunction(_, msg) -> (
report ~level:1 msg;
true, l (* keeping everything. *)
)
@@ -819,7 +819,7 @@ let rec build_switch_sys
other mem, one need to select the same guard g with the same
status b, *)
let res =
- if List.for_all (fun (m,mdefs) ->
+ if List.for_all (fun (_, mdefs) ->
(* All defs are unguarded *)
match mdefs with
| [[], _] -> true (* Regular unguarded expression *)
@@ -1087,7 +1087,7 @@ let merge_updates sys =
[mk_binop "&&"
(List.map export gl)]
in
- let rec clean_disj disj =
+ let clean_disj disj =
match disj with
| [] -> []
| [_] -> assert false (* A disjunction with a single case can be ignored *)
diff --git a/src/tools/stateflow/models/model_simple.ml b/src/tools/stateflow/models/model_simple.ml
index c2624f8dcbc1ef9bdd2b9121adc2226c413035b4..83d940992fe2bbf5726ac2522262619a603d6b37 100644
--- a/src/tools/stateflow/models/model_simple.ml
+++ b/src/tools/stateflow/models/model_simple.ml
@@ -4,7 +4,7 @@ open SF
let name = "simple"
-let condition x = condition {
+let condition _ = condition {
expr = Corelang.mkexpr Location.dummy_loc (Lustre_types.Expr_const (Corelang.const_of_bool true));
cinputs = [];
coutputs = [];
diff --git a/src/tools/stateflow/models/model_stopwatch.ml b/src/tools/stateflow/models/model_stopwatch.ml
index 7c468570ef7ba8a562c81e56637c9db24e91efde..2e1d6cd1021195e35a7aa0a08df0c9567329ee1d 100644
--- a/src/tools/stateflow/models/model_stopwatch.ml
+++ b/src/tools/stateflow/models/model_stopwatch.ml
@@ -4,9 +4,9 @@ open Basetypes
open SF
let verbose = false
-let actionv x = no_action (*TODO if verbose then action x else no_action*)
-let action x = no_action (* TODO *)
-let condition x = condition {
+let actionv _ = no_action (*TODO if verbose then action x else no_action*)
+let action _ = no_action (* TODO *)
+let condition _ = condition {
expr = Corelang.mkexpr Location.dummy_loc (Lustre_types.Expr_const (Corelang.const_of_bool true));
cinputs = [];
coutputs = [];
diff --git a/src/tools/stateflow/semantics/cPS.ml b/src/tools/stateflow/semantics/cPS.ml
index b73c250748313d74fc06bc6d44cf6c3bd2afdae0..723887fabac2a17e0dfa259dc5b88cddc23295b1 100644
--- a/src/tools/stateflow/semantics/cPS.ml
+++ b/src/tools/stateflow/semantics/cPS.ml
@@ -27,9 +27,9 @@ let eval ((modular_entry:bool), (modular_during:bool), (modular_exit:bool)) =
let modular : type b. (path_t, b, bool) tag_t -> path_t -> b =
fun tag ->
match tag with
- | E -> (fun p p' f -> modular_entry)
- | D -> (fun p -> modular_during)
- | X -> (fun p f -> modular_exit)
+ | E -> (fun _p _p' _f -> modular_entry)
+ | D -> (fun _p -> modular_during)
+ | X -> (fun _p _f -> modular_exit)
end
in
let module Thetaify = KenvTheta.ModularThetaify (Tables) (Modularity) in
diff --git a/src/tools/stateflow/semantics/cPS_ccode_generator.ml b/src/tools/stateflow/semantics/cPS_ccode_generator.ml
index 1704598a09468cf6958405e1b39dd662f1e8ef7d..df96e3236184ffe076ba484dafff7ad75fb77313 100644
--- a/src/tools/stateflow/semantics/cPS_ccode_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_ccode_generator.ml
@@ -1,5 +1,3 @@
-open Basetypes
-open ActiveStates
open CPS_transformer
module CodeGenerator : ComparableTransformerType =
@@ -23,44 +21,44 @@ struct
| _ , Seq trl2 -> Seq (tr1::trl2)
| _ -> Seq ([tr1;tr2])
- let rec ( == ) tr1 tr2 = tr1 = tr2
+ let ( == ) tr1 tr2 = tr1 = tr2
- let eval_act kenv (action : act_t) =
+ let eval_act _kenv (action : act_t) =
(*Format.printf "----- action = %a@." Action.pp_act action;*)
Act action
(*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
- let rec eval_cond condition ok ko =
+ let eval_cond condition ok ko =
(*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
Ite (condition, ok, ko)
- let rec pp_transformer fmt tr =
- match tr with
- | Bot -> Format.fprintf fmt "bot"
- | Act a ->
- Format.fprintf fmt "<%a>" pp_act a
- | Seq trl ->
- Format.fprintf fmt "@[<v 0>%a@]"
- (Utils.fprintf_list ~sep:";@ " pp_transformer)
- trl
- | Ite (c, t, e) ->
- Format.fprintf fmt "@[<v 0>if %a@ @[<v 2>then@ %a@]@ @[<v 2>else@ %a@]@ endif@]" pp_cond c pp_transformer t pp_transformer e
+ (* let rec pp_transformer fmt tr =
+ * match tr with
+ * | Bot -> Format.fprintf fmt "bot"
+ * | Act a ->
+ * Format.fprintf fmt "<%a>" pp_act a
+ * | Seq trl ->
+ * Format.fprintf fmt "@[<v 0>%a@]"
+ * (Utils.fprintf_list ~sep:";@ " pp_transformer)
+ * trl
+ * | Ite (c, t, e) ->
+ * Format.fprintf fmt "@[<v 0>if %a@ @[<v 2>then@ %a@]@ @[<v 2>else@ %a@]@ endif@]" pp_cond c pp_transformer t pp_transformer e *)
- let pp_principal fmt tr =
- Format.fprintf fmt "principal =@.%a" pp_transformer tr
+ (* let pp_principal fmt tr =
+ * Format.fprintf fmt "principal =@.%a" pp_transformer tr *)
- let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
- fun fmt call -> match call with
- | Ecall -> (fun (p, p', f) tr ->
- Format.fprintf fmt "component %a(%a, %a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)
- | Dcall -> (fun p tr ->
- Format.fprintf fmt "component %a(%a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_transformer tr)
- | Xcall -> (fun (p, f) tr ->
- Format.fprintf fmt "component %a(%a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_frontier f pp_transformer tr)
+ (* let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
+ * fun fmt call -> match call with
+ * | Ecall -> (fun (p, p', f) tr ->
+ * Format.fprintf fmt "component %a(%a, %a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)
+ * | Dcall -> (fun p tr ->
+ * Format.fprintf fmt "component %a(%a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_transformer tr)
+ * | Xcall -> (fun (p, f) tr ->
+ * Format.fprintf fmt "component %a(%a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_frontier f pp_transformer tr) *)
let mkcomponent _ = assert false
let mkprincipal _ = assert false
- let mktransformer _ = assert false
+ (* let mktransformer _ = assert false *)
end
diff --git a/src/tools/stateflow/semantics/cPS_interpreter.ml b/src/tools/stateflow/semantics/cPS_interpreter.ml
index 5caff1808acf5cc22c269b21c8b4cd42fd2348ae..f6a91d974f5cea5aa4d0a7da66f8292734da7675 100644
--- a/src/tools/stateflow/semantics/cPS_interpreter.ml
+++ b/src/tools/stateflow/semantics/cPS_interpreter.ml
@@ -142,7 +142,7 @@ struct
| Or (_T, []) -> null
| Or ([], [s0]) -> eval_open_path Enter prefix [] [s0] null
| Or (_T, _S) -> let wrapper = eval_open_path Enter [] prefix in
- let success p_d = null in
+ let success _p_d = null in
eval_T _T wrapper success { local = bot; global = bot }
| And (_S) -> List.fold_right (fun p -> (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null
)
@@ -174,7 +174,7 @@ struct
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p);
let wrapper_i = eval_open_path Inner [] p in
let wrapper_o = eval_open_path Outer [] p in
- let success p_d = null in
+ let success _p_d = null in
let fail_o =
let fail_i =
let same_fail_C = eval_C D p p_def.internal_composition in
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.ml b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
index 6d88a593f3e109481f7e68255850b7e0a95cfb26..4d650242a376713c6194f51c3eb440582d093ee0 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
@@ -1,5 +1,4 @@
open Basetypes
-open ActiveStates
open CPS_transformer
let ff = Format.fprintf
@@ -23,7 +22,7 @@ struct
((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
(fun () -> cpt := 0))
- let new_aut, reset_aut =
+ let new_aut, _reset_aut =
let cpt = ref 0 in
((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt),
(fun () -> cpt := 0))
@@ -33,13 +32,13 @@ struct
prefix
(fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
- let pp_typed_path sin fmt path =
- Format.fprintf fmt "%a : bool" (pp_path sin) path
+ (* let pp_typed_path sin fmt path =
+ * Format.fprintf fmt "%a : bool" (pp_path sin) path *)
- let pp_vars sin fmt vars =
- Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars))
- let pp_vars_decl sin fmt vars =
- Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))
+ (* let pp_vars sin fmt vars =
+ * Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars)) *)
+ (* let pp_vars_decl sin fmt vars =
+ * Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars)) *)
let var_to_ident prefix p =
pp_path prefix Format.str_formatter p;
@@ -140,7 +139,7 @@ struct
)
let bot sin sout =
- let (vars, tr) = null sin sout in
+ let _, tr = null sin sout in
(
ActiveStates.Vars.empty,
{ tr with assert_false = true }
@@ -148,8 +147,8 @@ struct
let ( >> ) tr1 tr2 sin sout =
let l = new_loc () in
- let (vars1, tr1) = tr1 sin l in
- let (vars2, tr2) = tr2 l sout in
+ let vars1, tr1 = tr1 sin l in
+ let vars2, tr2 = tr2 l sout in
(ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2),
{
statements = tr1.statements @ tr2.statements;
@@ -238,11 +237,11 @@ struct
let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in
mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
- let eval_act kenv (action : act_t) =
+ let eval_act _kenv (action : act_t) =
(*Format.printf "----- action = %a@." Action.pp_act action;*)
(fun sin sout -> (ActiveStates.Vars.empty,
- mkact' action sin sout ))
-
+ mkact' action sin sout ))
+
let rec mkcond' sin condition =
(*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
match condition with
@@ -258,13 +257,13 @@ struct
mkcond' sin cond2]
| Condition.Quote c -> c.expr (* TODO: shall we prefix with sin ? *)
- let rec eval_cond condition (ok:t) ko sin sout =
+ let eval_cond condition (ok:t) ko sin sout =
let open Lustre_types in
let loc = Location.dummy_loc in
(*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
- let (vars1, tr1) = ok sin sout in
- let (vars2, tr2) = ko sin sout in
- let (vars0, tr0) = bot sin sout in
+ let vars1, tr1 = ok sin sout in
+ let vars2, tr2 = ko sin sout in
+ let _, tr0 = bot sin sout in
let aut = new_aut () in
(ActiveStates.Vars.empty,
{
@@ -316,9 +315,9 @@ struct
}
)
- let mktransformer tr =
- let (vars, tr) = tr "sin_" "sout_"
- in tr
+ (* let mktransformer tr =
+ * let _, tr = tr "sin_" "sout_"
+ * in tr *)
let mkcomponent :
type c. c call_t -> c -> t -> Lustre_types.program_t =
diff --git a/src/tools/stateflow/semantics/cPS_transformer.ml b/src/tools/stateflow/semantics/cPS_transformer.ml
index 1191df5f4d88f0e52848e8c8127656ad2e1dd54d..a1082dc7df9bfb5db3213795cb974471277b587c 100644
--- a/src/tools/stateflow/semantics/cPS_transformer.ml
+++ b/src/tools/stateflow/semantics/cPS_transformer.ml
@@ -1,5 +1,4 @@
open Basetypes
-open ActiveStates
type mode_t =
| Outer
diff --git a/src/tools/stateflow/semantics/theta.ml b/src/tools/stateflow/semantics/theta.ml
index 27c855fb9d32b7b43c42a7b965c271fc3785b871..6108d032204f4eaeb06c61b2dab55c79ceb2fb9a 100644
--- a/src/tools/stateflow/semantics/theta.ml
+++ b/src/tools/stateflow/semantics/theta.ml
@@ -150,7 +150,7 @@ struct
let theta tag = theta_ify Kenv.kenv tag
- let components call = []
+ let components _call = []
end
module ModularThetaify : functor (Tables : MemoThetaTablesType) (Mod : ModularType) -> ThetaifyType =
diff --git a/src/tools/stateflow/sf_sem.ml b/src/tools/stateflow/sf_sem.ml
index f09fc284843d2ce9c22ea2a3c1c5b43a41190adc..45eab193e83ade312e7d70cc440071be8eb16100 100644
--- a/src/tools/stateflow/sf_sem.ml
+++ b/src/tools/stateflow/sf_sem.ml
@@ -82,7 +82,7 @@ let _ =
Format.fprintf auto_fmt "%a@." Printers.pp_prog prog;
let params = Backends.get_normalization_params () in
- let prog, deps = Compiler_stages.stage1 params prog "" "" ".lus" in
+ let prog, _ = Compiler_stages.stage1 params prog "" "" ".lus" in
Options.print_dec_types := false;
diff --git a/src/tools/zustre/zustre_cex.ml b/src/tools/zustre/zustre_cex.ml
index 680f7ca0c1572aa386e047a634e016c99f683c76..9556e1023cbb238be6dde137a5a2caed6e9023ee 100644
--- a/src/tools/zustre/zustre_cex.ml
+++ b/src/tools/zustre/zustre_cex.ml
@@ -19,7 +19,7 @@ let get_conjuncts e =
else
[e]
-let build_cex machine machines decl_err =
+let build_cex machine machines _decl_err =
(* Recovering associated top machine (to build full traces) and property *)
(* TODO: for example extract top node and ok prop. We may have multiple
MAIN/ERR loaded at the same time. Each of them should be assocaited with a
@@ -46,7 +46,7 @@ let build_cex machine machines decl_err =
let nb_outputs = List.length inputs in
let nb_mems = List.length (full_memory_vars machines machine) in
- let main, funs =
+ let main, _ =
List.fold_left (fun (main, funs) conj ->
(* Filtering out non MAIN decls *)
let func_decl = Z3.Expr.get_func_decl conj in
@@ -90,7 +90,7 @@ let build_cex machine machines decl_err =
(* We recover the Zustre XML format, projecting each cex on each input/output
signal *)
- let in_signals, out_signals =
+ let in_signals, _ =
List.fold_right (
fun (id, (sigs_in, sigs_out)) (res_sigs_in, res_sigs_out) ->
let add l1 l2 = List.map2 (fun e1 e2 -> fst e2, ((id, e1)::(snd e2))) l1 l2 in
@@ -158,7 +158,7 @@ let build_cex machine machines decl_err =
(* (Z3.Statistics.Entry.to_string e) *)
(* ) stats_entries; *)
- let json : Yojson.json =
+ let json : Yojson.t =
`Assoc [
"Results",
`Assoc [
diff --git a/src/tools/zustre/zustre_common.ml b/src/tools/zustre/zustre_common.ml
index d8eed30ae6b272cb840aac84e2c4805d46510be4..959c5b91a18fcec31a6908be82f5397284f213a2 100644
--- a/src/tools/zustre/zustre_common.ml
+++ b/src/tools/zustre/zustre_common.ml
@@ -1,7 +1,6 @@
open Lustre_types
open Machine_code_types
open Machine_code_common
-open Format
(* open Horn_backend_common
* open Horn_backend *)
open Zustre_data
@@ -87,8 +86,8 @@ let rec type_to_sort t =
match (Types.repr t).Types.tdesc with
| Types.Tconst ty -> get_const_sort ty
| Types.Tclock t -> type_to_sort t
- | Types.Tarray(dim,ty) -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
- | Types.Tstatic(d, ty)-> type_to_sort ty
+ | Types.Tarray(_, ty) -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
+ | Types.Tstatic(_, ty) -> type_to_sort ty
| Types.Tarrow _
| _ -> Format.eprintf "internal error: pp_type %a@."
Types.print_ty t; assert false
@@ -221,7 +220,7 @@ let horn_tag_to_expr t =
match res with None -> assert false | Some s -> s
(* Prints a constant value *)
-let rec horn_const_to_expr c =
+let horn_const_to_expr c =
match c with
| Const_int i -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
| Const_real r -> Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)
@@ -234,7 +233,7 @@ let rec horn_const_to_expr c =
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
for the type integer (arrays).
*)
-let rec horn_default_val t =
+let horn_default_val t =
let t = Types.dynamic_type t in
if Types.is_bool_type t then Z3.Boolean.mk_true !ctx else
if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else
@@ -397,7 +396,7 @@ let rec horn_val_to_expr ?(is_lhs=false) m self v =
(* Code specific for arrays *)
- | Power (v, n) -> assert false
+ | Power _ -> assert false
| Var v ->
if is_memory m v then
if Types.is_array_type v.var_type
@@ -524,7 +523,7 @@ let instance_call_to_exprs machines reset_instances m i inputs outputs =
[stmt1; stmt2]
end
- | node_name_n ->
+ | _ ->
let expr =
Z3.Expr.mk_app
!ctx
@@ -600,7 +599,7 @@ let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.e
m
(mk_val (Var i) i.var_type) v,
reset_instances
- | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
+ | MStep ([_], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
assert false (* This should not happen anymore *)
| MStep (il, i, vl) ->
(* if reset instance, just print the call over mem_m , otherwise declare mem_m =
@@ -676,10 +675,11 @@ let add_rule ?(dont_touch=[]) vars expr =
(* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)
(* New code: we extract vars from expr *)
- let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
- let compare = compare
- let hash = Hashtbl.hash
- end)
+ let module FDSet = Set.Make (struct
+ type t = Z3.FuncDecl.func_decl
+ let compare = compare
+ (* let hash = Hashtbl.hash *)
+ end)
in
(* Fonction seems unused
@@ -752,7 +752,7 @@ let add_rule ?(dont_touch=[]) vars expr =
(********************************************************)
let machine_reset machines m =
- let locals = local_memory_vars machines m in
+ let locals = local_memory_vars m in
(* print "x_m = x_c" for each local memory *)
let mid_mem_def =
@@ -810,7 +810,7 @@ let decl_machine machines m =
let _ =
List.map decl_var
(
- (inout_vars machines m)@
+ (inout_vars m)@
(rename_current_list (full_memory_vars machines m)) @
(rename_mid_list (full_memory_vars machines m)) @
(rename_next_list (full_memory_vars machines m)) @
@@ -823,7 +823,7 @@ let decl_machine machines m =
Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
(* Declaring single predicate *)
- let vars = inout_vars machines m in
+ let vars = inout_vars m in
let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
diff --git a/src/tools/zustre/zustre_verifier.ml b/src/tools/zustre/zustre_verifier.ml
index 337654c956505e4897f6e83364fb29874c82b45b..3690f9d7085b055bf88bc5b81b972e7d817ab1e0 100644
--- a/src/tools/zustre/zustre_verifier.ml
+++ b/src/tools/zustre/zustre_verifier.ml
@@ -158,7 +158,7 @@ module Verifier =
Z3.Fixedpoint.set_parameters !fp fp_params
- let run ~basename prog machines =
+ let run ~basename _prog machines =
let machines = Machine_code_common.arrow_machine::machines in
let machines = preprocess machines in
setup_solver ();
diff --git a/src/types.ml b/src/types.ml
index 69dd4cfc1446f99a94542cf51e9ce2f48a570f28..be2fe4acc86a389a9ae313695384d74d16288445 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -169,7 +169,7 @@ and print_ty_param pp_basic fmt ty =
| Tbasic t -> pp_basic fmt t
| Tclock t ->
fprintf fmt "%a%s" print_ty t (if !Options.kind2_print then "" else " clock")
- | Tstatic (d, t) -> print_ty fmt t
+ | Tstatic (_, t) -> print_ty fmt t
(* fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t *)
| Tconst t ->
fprintf fmt "%s" t
@@ -257,7 +257,7 @@ let pp_error fmt = function
| Type_clash (ty1,ty2) ->
Utils.reset_names ();
fprintf fmt "Expected type %a, got type %a@." print_ty ty1 print_ty ty2
- | Poly_imported_node id ->
+ | Poly_imported_node _ ->
fprintf fmt "Imported nodes cannot have a polymorphic type@."
@@ -277,7 +277,7 @@ let new_univar () =
let rec repr =
function
- {tdesc = Tlink t'} ->
+ {tdesc = Tlink t'; _} ->
repr t'
| t -> t
@@ -291,10 +291,10 @@ let get_field_type ty label =
| Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
| _ -> None
-let rec is_static_type ty =
+let is_static_type ty =
match (repr ty).tdesc with
- | Tstatic (_, ty) -> true
- | _ -> false
+ | Tstatic _ -> true
+ | _ -> false
let rec is_scalar_type ty =
match (repr ty).tdesc with
diff --git a/src/typing.ml b/src/typing.ml
index f80efb4d19831bd653f899e3b0782a35fb57a50e..f5d7a164793d4bc6f10a878392ac988dac46a6d1 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -14,7 +14,7 @@
(** Main typing module. Classic inference algorithm with destructive
unification. *)
-let debug fmt args = () (* Format.eprintf "%a" *)
+let debug _fmt _args = () (* Format.eprintf "%a" *)
(* Though it shares similarities with the clock calculus module, no code
is shared. Simple environments, very limited identifier scoping, no
identifier redefinition allowed. *)
@@ -24,7 +24,6 @@ open Utils
overwritten, yet this makes notations far lighter.*)
open Lustre_types
open Corelang
-open Format
(* TODO general remark: except in the add_vdecl, it seems to me that
@@ -64,7 +63,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
| Ttuple tl ->
List.exists (occurs tvar) tl
| Tstruct fl ->
- List.exists (fun (f, t) -> occurs tvar t) fl
+ List.exists (fun (_, t) -> occurs tvar t) fl
| Tarray (_, t)
| Tstatic (_, t)
| Tclock t
@@ -84,7 +83,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
| Ttuple tl ->
List.iter generalize tl
| Tstruct fl ->
- List.iter (fun (f, t) -> generalize t) fl
+ List.iter (fun (_, t) -> generalize t) fl
| Tstatic (d, t)
| Tarray (d, t) -> Dimension.generalize d; generalize t
| Tclock t
@@ -171,7 +170,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
let get_type_definition tname =
- type_coretype (fun d -> ()) (get_coretype_definition tname)
+ type_coretype (fun _ -> ()) (get_coretype_definition tname)
(* Equality on ground types only *)
(* Should be used between local variables which must have a ground type *)
@@ -216,7 +215,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
(* strictly subtyping cases first *)
| _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
unif t1 t2
- | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
+ | _ , Tstatic (_, t2) when sub && (get_static_value t1 = None) ->
unif t1 t2
(* This case is not mandatory but will keep "older" types *)
| Tvar, Tvar ->
@@ -256,7 +255,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
let eval_const =
if semi
then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
- else (fun c -> None) in
+ else (fun _ -> None) in
begin
unif t1' t2';
Dimension.eval Basic_library.eval_dim_env eval_const e1;
@@ -290,10 +289,10 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
then let tydef = Hashtbl.find field_table label in
let tydec = (typedef_of_top tydef).tydef_desc in
let tydec_struct = get_struct_type_fields tydec in
- let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
+ let ty_label = type_coretype (fun _ -> ()) (List.assoc label tydec_struct) in
begin
try_unify ty_label (type_const ~is_annot loc c) loc;
- type_coretype (fun d -> ()) tydec
+ type_coretype (fun _ -> ()) tydec
end
else raise (Error (loc, Unbound_value ("struct field " ^ label)))
@@ -313,7 +312,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
if is_user_type tydef.tydef_desc
then Tydec_const tydef.tydef_id
else tydef.tydef_desc in
- type_coretype (fun d -> ()) tydec
+ type_coretype (fun _ -> ()) tydec
else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
| Const_struct fl ->
let ty_struct = new_var () in
@@ -363,7 +362,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
(match (* Types. *)get_static_value targ with
| None -> ()
- | Some d' -> try_unify targ real_static_type arg.expr_loc);
+ | Some _ -> try_unify targ real_static_type arg.expr_loc);
real_static_type
else targ
@@ -704,10 +703,10 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
*)
env
- let rec type_spec env spec loc =
+ let rec type_spec env spec =
match spec with
| Contract c -> type_contract env c
- | NodeSpec id -> env
+ | NodeSpec _ -> env
(** [type_node env nd loc] types node [nd] in environment env. The
location is used for error reports. *)
@@ -728,7 +727,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
(fun uvs v -> ISet.add v.var_id uvs)
ISet.empty vd_env_ol in
let undefined_vars =
- let eqs, auts = get_node_eqs nd in
+ let eqs, _ = get_node_eqs nd in
(* TODO XXX: il faut typer les handlers de l'automate *)
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init eqs
in
@@ -740,7 +739,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
(* Typing spec/contracts *)
(match nd.node_spec with
| None -> ()
- | Some spec -> ignore (type_spec new_env spec loc));
+ | Some spec -> ignore (type_spec new_env spec));
(* Typing annots *)
List.iter (fun annot ->
List.iter (fun (_, eexpr) -> ignore (type_eexpr (new_env, vd_env) eexpr)) annot.annots
@@ -760,7 +759,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
nd.node_type <- Expr_type_hub.export ty_node;
Env.add_value env nd.node_id ty_node
- let type_imported_node env nd loc =
+ let type_imported_node env nd _loc =
let vd_env = nd.nodei_inputs@nd.nodei_outputs in
check_vd_env vd_env;
let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in
@@ -769,7 +768,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
(* Typing spec *)
(match nd.nodei_spec with
| None -> ()
- | Some spec -> ignore (type_spec new_env spec loc));
+ | Some spec -> ignore (type_spec new_env spec));
let ty_ins = type_of_vlist nd.nodei_inputs in
let ty_outs = type_of_vlist nd.nodei_outputs in
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
@@ -801,7 +800,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
| Node nd -> (
try
type_node env nd decl.top_decl_loc
- with Error (loc, err) as exc -> (
+ with Error _ as exc -> (
if !Options.global_inline then
Format.eprintf "Type error: failing node@.%a@.@?"
Printers.pp_node nd
diff --git a/src/utils/dimension.ml b/src/utils/dimension.ml
index 4a46d85aedf9aa4421866b21b01d63c6a1cd1a62..d97d27d82f372b3197dbd505decb15c0f608cd8a 100644
--- a/src/utils/dimension.ml
+++ b/src/utils/dimension.ml
@@ -174,14 +174,14 @@ let rec factors_constant fs =
let norm_factors fs =
let k = factors_constant fs in
let nk = List.filter (fun d -> not (is_dimension_const d)) fs in
- (k, List.sort Pervasives.compare nk)
+ (k, List.sort compare nk)
let rec terms dim =
match dim.dim_desc with
| Dappl (f, args) when f = "+" -> List.flatten (List.map terms args)
| _ -> [dim]
-let rec normalize dim =
+let normalize dim =
dim
(*
let rec unnormalize loc l =
@@ -295,7 +295,7 @@ let rec instantiate inst_dim_vars dim =
(instantiate inst_dim_vars t)
(instantiate inst_dim_vars e)
| Dappl (f, args) -> mkdim_appl dim.dim_loc f (List.map (instantiate inst_dim_vars) args)
- | Dlink dim' -> assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*)
+ | Dlink _ -> assert false (*mkdim dim.dim_loc (Dlink (instantiate inst_dim_vars dim'))*)
| Dunivar ->
try
List.assoc dim.dim_id !inst_dim_vars
diff --git a/src/utils/env.ml b/src/utils/env.ml
index 38c038087bcd66c25a51548528f6b82e131dcab8..687be6418251336c575fc677a86ec906582f6bc7 100644
--- a/src/utils/env.ml
+++ b/src/utils/env.ml
@@ -33,13 +33,11 @@ let fold = IMap.fold
overwrites definitions in x by definitions in y *)
let overwrite x y =
IMap.merge (
- fun k _old _new -> match _new with
+ fun _ _old _new -> match _new with
| Some _ -> _new
| _ -> _old
) x y
-open Format
-
let pp_env pp_fun fmt env =
let (lid,lty) = list_of_imap env in
let l' = List.combine lid lty in
diff --git a/src/utils/utils.ml b/src/utils/utils.ml
index f1c661dcde4f30e770de2ff32758331fc482c984..9125fb15c66bf9a2ac691843c768cd43095eba33 100644
--- a/src/utils/utils.ml
+++ b/src/utils/utils.ml
@@ -257,7 +257,7 @@ let pp_final_char_if_non_empty c l =
let pp_newline_if_non_empty l =
(fun fmt -> match l with [] -> () | _ -> Format.fprintf fmt "@,")
-let fprintf_list ?(eol:('a, formatter, unit) Pervasives.format = "") ~sep:sep f fmt l =
+let fprintf_list ?(eol:('a, formatter, unit) format = "") ~sep:sep f fmt l =
let rec aux fmt = function
| [] -> ()
| [e] -> f fmt e
diff --git a/src/verifiers.ml b/src/verifiers.ml
index baac4bc0a9de1e89c543cfe4a9a58207ce3e6a47..1b08d68cdfa5048d028f7ca02afc25eeca455c19 100644
--- a/src/verifiers.ml
+++ b/src/verifiers.ml
@@ -1,5 +1,3 @@
-open Lustre_types
-
open VerifierList
let () = Sites.Plugins.Verifiers.load_all ()