diff --git a/src/Makefile-lustresf.in b/src/Makefile-lustresf.in deleted file mode 100644 index e878cd751c2e02dcbb531d919b1288e7825d1f62..0000000000000000000000000000000000000000 --- a/src/Makefile-lustresf.in +++ /dev/null @@ -1,19 +0,0 @@ -lustresf: - @echo Compiling binary lustresf - @$(OCAMLBUILD) tools/stateflow/sf_sem.native - @mkdir -p $(LOCAL_BINDIR) - @mv _build/tools/stateflow/sf_sem.native $(LOCAL_BINDIR)/lustresf - -json-parser: - @echo Compiling binary json-parser-ex - @$(OCAMLBUILD) tools/stateflow/json-parser/main_parse_json_file.native - @mkdir -p $(LOCAL_BINDIR) - @mv _build/tools/stateflow/json-parser/main_parse_json_file.native $(LOCAL_BINDIR)/json-parser - -tests: test-simple-var - -test-simple-var: - @echo Compiling simple tests for JSON parser -- tests on variables - @$(OCAMLBUILD) tools/stateflow/json-parser/test_json_parser_variables.native - @echo Lauching simple tests for JSON parser -- tests on variables - ./_build/tools/stateflow/json-parser/test_json_parser_variables.native diff --git a/src/Makefile.in b/src/Makefile.in deleted file mode 100644 index f6fbf5908b1a512d2e59cd52af5ab887c47c65d6..0000000000000000000000000000000000000000 --- a/src/Makefile.in +++ /dev/null @@ -1,61 +0,0 @@ -OCAMLBUILD=@OCAMLBUILD@ -use-ocamlfind -no-links - -prefix=@prefix@ -exec_prefix=@exec_prefix@ -bindir=@bindir@ -datarootdir = ${prefix}/share -includedir = ${prefix}/include - -LUSI_LIBS=include/math.lusi include/conv.lusi -LOCAL_BINDIR=../bin -LOCAL_DOCDIR=../doc/manual - -all: lustrec lustret lustrev - -lustrec: - @echo Compiling binary lustrec - @$(OCAMLBUILD) main_lustre_compiler.native - @mkdir -p $(LOCAL_BINDIR) - @mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec - -lustret: - @echo Compiling binary lustret - @$(OCAMLBUILD) main_lustre_testgen.native - @mkdir -p $(LOCAL_BINDIR) - @mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret - -lustrev: - @echo Compiling binary lustrev - @$(OCAMLBUILD) main_lustre_verifier.native - @mkdir -p $(LOCAL_BINDIR) - @mv _build/main_lustre_verifier.native $(LOCAL_BINDIR)/lustrev - -lustrei: - @echo Compiling binary lustrei - @$(OCAMLBUILD) tools/importer/main_lustre_importer.native - @mkdir -p $(LOCAL_BINDIR) - @mv _build/tools/importer/main_lustre_importer.native $(LOCAL_BINDIR)/lustrei - -@lustresf_src@ - -doc: - @echo Generating doc - @$(OCAMLBUILD) lustrec.docdir/index.html - @rm -rf $(LOCAL_DOCDIR) - @cp -rf _build/lustrec.docdir $(LOCAL_DOCDIR) - -dot: doc - $(OCAMLBUILD) lustrec.docdir/lustrec.dot - dot -T svg -o $(LOCAL_DOCDIR)/lustrec.svg _build/lustrec.docdir/lustrec.dot - -clean: - $(OCAMLBUILD) -clean - -dist-clean: clean - rm -f Makefile myocamlbuild.ml config.log config.status configure - rm -f include/*.lusic include/math.h include/conv.h - -install: - make -C .. install - -.PHONY: compile-lusi doc dot lustrec lustret lustrev lustrec.odocl clean install dist-clean tests diff --git a/src/_tags.in b/src/_tags.in deleted file mode 100644 index 508a48b45e29f124cdf4c1ae85d96d95a0e408e0..0000000000000000000000000000000000000000 --- a/src/_tags.in +++ /dev/null @@ -1,73 +0,0 @@ -# general config -true: bin_annot, color(always) -# true: use_menhir - -# paths to sources -"utils": include -"checks": include -"parsers": include -"backends": include -"backends/Ada": include -"backends/C": include -"backends/Horn": include -"backends/EMF": include -"backends/VHDL": include -"plugins/salsa": include -"plugins/scopes": include -"plugins/mpfr": include -"features/machine_types": include -"tools": include -"tools/zustre": include -"tools/stateflow": include -"tools/stateflow/common": include -"tools/stateflow/semantics": include -"tools/stateflow/models": include -"tools/stateflow/json-parser": include -"tools/importer": include -"tools/seal": include -"tools/tiny": include - -# svn -<**/.svn>: -traverse -<**/.svn>: not_hygienic - -# packages -<**/*.native> or <**/*.ml{,i}> : package(num) -<**/*.native> or <**/*.ml{,i}> : package(ocamlgraph) -<**/*verifier.native> or <**/*.ml{,i}> : package(yojson) -<**/*verifier.native>: thread - -# <**/*.native> : use_str -<**/main_lustre_compiler.native>: package(unix,str) -<**/main_lustre_testgen.native> : package(unix,str) -<**/main_lustre_verifier.native> : package(unix,str) -<**/sf_sem.native> : package(unix) -<**/*> : package(num) -<**/*> : package(zarith) -<**/*.ml> : package(logs) -<**/*.native> : package(logs) -<**/json_parser.ml> : package(yojson) -<**/main_parse_json_file.*> : package(cmdliner) -<**/main_parse_json_file.*> : package(fmt.tty) -<**/main_parse_json_file.*> : package(fmt.cli) -<**/main_parse_json_file.*> : package(logs.fmt) -<**/main_parse_json_file.*> : package(logs.cli) -<**/main_parse_json_file.*> : package(yojson) -<**/test_*.*> : package(oUnit) -<**/test_json*.*> : package(yojson) - -# Required for ocamldoc. Otherwise failed to build -<**/*.ml{,i}>: package(ocamlgraph) -<**/*.ml{,i}>: package(num) - -# Plugin dependencies -@SALSA_TAG@ - -# Available solvers -@LUSTREV_SEAL_TAG@ -@LUSTREV_TINY_TAG@ -@LUSTREV_Z3_TAG@ - -# Local Variables: -# mode: conf -# End: diff --git a/src/backends/Ada/ada_backend.ml b/src/backends/Ada/ada_backend.ml index a94b1b121142d7d028ea41881f655cbe750df950..53e4265e239c8e0297c52a9d724cd87527dea5d3 100644 --- a/src/backends/Ada/ada_backend.ml +++ b/src/backends/Ada/ada_backend.ml @@ -71,20 +71,23 @@ let extract_contract machines m = | _ :: t -> find_submachine_from_ident ident t in - let extract_ident eexpr = - match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with - | Expr_ident ident -> - ident - | _ -> - assert false - (* | Expr_const cst -> assert false | Expr_tuple exprs -> assert false | - Expr_ite (expr1, expr2, expr3) -> assert false | Expr_arrow (expr1, - expr2) -> assert false | Expr_fby (expr1, expr2) -> assert false | - Expr_array exprs -> assert false | Expr_access (expr1, dim) -> assert - false | Expr_power (expr1, dim) -> assert false | Expr_pre expr -> assert - false | Expr_when (expr,ident,label) -> assert false | Expr_merge (ident, - l) -> assert false | Expr_appl call -> assert false *) - in + (* XXX: UNUSED *) + (* let extract_ident eexpr = *) + (* match eexpr.Lustre_types.eexpr_qfexpr.expr_desc with *) + (* | Expr_ident ident -> *) + (* ident *) + (* | _ -> *) + (* assert false *) + (* (\* | Expr_const cst -> assert false | Expr_tuple exprs -> assert false | *) + (* Expr_ite (expr1, expr2, expr3) -> assert false | Expr_arrow (expr1, *) + (* expr2) -> assert false | Expr_fby (expr1, expr2) -> assert false | *) + (* Expr_array exprs -> assert false | Expr_access (expr1, dim) -> assert *) + (* false | Expr_power (expr1, dim) -> assert false | Expr_pre expr -> + assert *) + (* false | Expr_when (expr,ident,label) -> assert false | Expr_merge + (ident, *) + (* l) -> assert false | Expr_appl call -> assert false *\) *) + (* in *) match m.mspec.mnode_spec with | Some (NodeSpec ident) -> let machine_spec = find_submachine_from_ident ident machines in diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml index 3aea2cb79dcd874dd0902157162c85cf08b916a4..d1eef9e4a55665e1c47851f0385faccf524eb792 100644 --- a/src/backends/EMF/EMF_backend.ml +++ b/src/backends/EMF/EMF_backend.ml @@ -418,7 +418,8 @@ let pp_emf_spec_mode fmt m = fprintf fmt "\"require\": [%a]@ " pp_emf_eexprs m.require; fprintf fmt "@]}" -let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode +(* XXX: UNUSED *) +(* let pp_emf_spec_modes = pp_emf_list pp_emf_spec_mode *) (* XXX: UNUSED *) (* let pp_emf_spec_import fmt i = diff --git a/src/backends/EMF/EMF_backend.ml~ b/src/backends/EMF/EMF_backend.ml~ deleted file mode 100644 index b0295047782a5b1870bc8b670c949e37392b6cf7..0000000000000000000000000000000000000000 --- a/src/backends/EMF/EMF_backend.ml~ +++ /dev/null @@ -1 +0,0 @@ -let translate fmt prog diff --git a/src/lustrec.odocl b/src/lustrec.odocl deleted file mode 100644 index 9cb5a43ab8e4d8da3ada1ef67ef44e934c30cc0b..0000000000000000000000000000000000000000 --- a/src/lustrec.odocl +++ /dev/null @@ -1,69 +0,0 @@ -Env -Version -Compiler_common -Location -Options_management -PluginList -Delay -Plugins -SortProg -Type_predef -Mutation -Basic_library -Normalization -Utils -Modules -Spec -Machine_code -backends/EMF/EMF_common -backends/EMF/EMF_library_calls -backends/EMF/EMF_backend -backends/Horn/Horn_backend_traces -backends/Horn/Horn_backend_printers -backends/Horn/Horn_backend_common -backends/Horn/Horn_backend -backends/Horn/Horn_backend_collecting_sem -backends/C/C_backend_lusic -backends/C/C_backend -backends/C/C_backend_src -backends/C/C_backend_common -backends/C/C_backend_main -backends/C/C_backend_makefile -backends/C/C_backend_header -backends/C/C_backend_mauve -backends/C/C_backend_spec -backends/Backends -Delay_predef -Options -Global -features/machine_types/Machine_types -PluginType -Main_lustre_testgen -Clock_calculus -plugins/scopes/Scopes -Types -AlgebraicLoop -Liveness -Main_lustre_compiler -Optimize_machine -PathConditions -Automata -Dimension -Clocks -Access -Parse -Corelang -Scheduling -Causality -Lusic -Error -Compiler_stages -Splitting -Stateless -Printers -Mmap -Typing -Inliner -Clock_predef -Ocaml_utils -Annotations diff --git a/src/features/machine_types/machine_types.ml b/src/machine_types.ml similarity index 98% rename from src/features/machine_types/machine_types.ml rename to src/machine_types.ml index ffd57311aad7532429d6becb8e2a38252d757e18..3700ef3558b2d1d643e65d75c414d1fe48358418 100644 --- a/src/features/machine_types/machine_types.ml +++ b/src/machine_types.ml @@ -276,13 +276,14 @@ let is_specified v = (* Format.eprintf "looking for var %a@." Printers.pp_var v; *) Hashtbl.mem machine_type_table v -let pp_table fmt = - Format.fprintf fmt "@[<v 0>["; - Hashtbl.iter - (fun v typ -> - Format.fprintf fmt "%a -> %a,@ " Printers.pp_var v MTypes.pp typ) - machine_type_table; - Format.fprintf fmt "@]" +(* XXX: UNUSED *) +(* let pp_table fmt = *) +(* Format.fprintf fmt "@[<v 0>["; *) +(* Hashtbl.iter *) +(* (fun v typ -> *) +(* Format.fprintf fmt "%a -> %a,@ " Printers.pp_var v MTypes.pp typ) *) +(* machine_type_table; *) +(* Format.fprintf fmt "@]" *) let get_specified_type v = (* Format.eprintf "Looking for variable %a in table [%t]@.@?" *) diff --git a/src/features/machine_types/machine_types.mli b/src/machine_types.mli similarity index 100% rename from src/features/machine_types/machine_types.mli rename to src/machine_types.mli diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml index e00aea1f7e7bbba58d2d2054b4bbeaacbeaeabbe..a98d07c5a01d0834ae9ef824f2f7742fbc3a2a00 100644 --- a/src/optimize_machine.ml +++ b/src/optimize_machine.ml @@ -1231,70 +1231,71 @@ let machines_clean prog = (* Additional function to modify the prog according to removed variables map *) -let elim_prog_variables prog removed_table = - List.map - (fun t -> - match t.top_decl_desc with - | Node nd -> ( - match IMap.find_opt nd.node_id removed_table with - | Some nd_elim_map -> - (* Iterating through the elim map to compute - the list of variables - to remove - the associated list of lustre definitions x = expr to - be used when removing these variables *) - let vars_to_replace, defs = - (* Recovering vid from node locals *) - IMap.fold - (fun v (_, eq) (accu_locals, accu_defs) -> - let locals = - try - List.find - (fun v' -> v'.var_id = v) - (List.map fst nd.node_locals) - :: accu_locals - with Not_found -> accu_locals - (* Variable v shall be a global constant, we do no need to - eliminate it from the locals *) - in - (* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc = - e.expr_loc } in *) - let defs = eq :: accu_defs in - locals, defs) - nd_elim_map - ([], []) - in - let node_locals, node_stmts = - List.fold_right - (fun stmt (locals, res_stmts) -> - match stmt with - | Aut _ -> - assert false (* should be processed by now *) - | Eq eq -> ( - match eq.eq_lhs with - | [] -> - assert false (* shall not happen *) - | [ lhs ] - when List.exists (fun v -> v.var_id = lhs) vars_to_replace - -> - (* We remove the def *) - ( List.filter (fun (v, _) -> v.var_id <> lhs) locals, - res_stmts ) - | _ -> - (* When more than one lhs we just keep the equation and do - not delete it *) - let eq_rhs = - substitute_expr vars_to_replace defs eq.eq_rhs - in - locals, Eq { eq with eq_rhs } :: res_stmts)) - nd.node_stmts - (nd.node_locals, []) - in - let nd' = { nd with node_locals; node_stmts } in - { t with top_decl_desc = Node nd' } - | None -> - t) - | _ -> - t) - prog +(* XXX: UNUSED *) +(* let elim_prog_variables prog removed_table = *) +(* List.map *) +(* (fun t -> *) +(* match t.top_decl_desc with *) +(* | Node nd -> ( *) +(* match IMap.find_opt nd.node_id removed_table with *) +(* | Some nd_elim_map -> *) +(* (\* Iterating through the elim map to compute - the list of variables *) +(* to remove - the associated list of lustre definitions x = expr to *) +(* be used when removing these variables *\) *) +(* let vars_to_replace, defs = *) +(* (\* Recovering vid from node locals *\) *) +(* IMap.fold *) +(* (fun v (_, eq) (accu_locals, accu_defs) -> *) +(* let locals = *) +(* try *) +(* List.find *) +(* (fun v' -> v'.var_id = v) *) +(* (List.map fst nd.node_locals) *) +(* :: accu_locals *) +(* with Not_found -> accu_locals *) +(* (\* Variable v shall be a global constant, we do no need to *) +(* eliminate it from the locals *\) *) +(* in *) +(* (\* xxx let new_eq = { eq_lhs = [v]; eq_rhs = e; eq_loc = *) +(* e.expr_loc } in *\) *) +(* let defs = eq :: accu_defs in *) +(* locals, defs) *) +(* nd_elim_map *) +(* ([], []) *) +(* in *) +(* let node_locals, node_stmts = *) +(* List.fold_right *) +(* (fun stmt (locals, res_stmts) -> *) +(* match stmt with *) +(* | Aut _ -> *) +(* assert false (\* should be processed by now *\) *) +(* | Eq eq -> ( *) +(* match eq.eq_lhs with *) +(* | [] -> *) +(* assert false (\* shall not happen *\) *) +(* | [ lhs ] *) +(* when List.exists (fun v -> v.var_id = lhs) vars_to_replace *) +(* -> *) +(* (\* We remove the def *\) *) +(* ( List.filter (fun (v, _) -> v.var_id <> lhs) locals, *) +(* res_stmts ) *) +(* | _ -> *) +(* (\* When more than one lhs we just keep the equation and do *) +(* not delete it *\) *) +(* let eq_rhs = *) +(* substitute_expr vars_to_replace defs eq.eq_rhs *) +(* in *) +(* locals, Eq { eq with eq_rhs } :: res_stmts)) *) +(* nd.node_stmts *) +(* (nd.node_locals, []) *) +(* in *) +(* let nd' = { nd with node_locals; node_stmts } in *) +(* { t with top_decl_desc = Node nd' } *) +(* | None -> *) +(* t) *) +(* | _ -> *) +(* t) *) +(* prog *) (*** Main function ***) diff --git a/src/tools/seal/seal_extract.ml b/src/tools/seal/seal_extract.ml index d7275fb96ba0fd23da6d41a7bace38ebd61a0a8a..ecc71ce6cc3d7d2c0a750397a50275093b9d8e17 100644 --- a/src/tools/seal/seal_extract.ml +++ b/src/tools/seal/seal_extract.ml @@ -7,7 +7,8 @@ open Zustre_data (* Switched system extraction: expression are memoized *) (*let expr_mem = Hashtbl.create 13*) -let add_init defs vid = Hashtbl.add defs vid [ [], IsInit ] +(* XXX: UNUSED *) +(* let add_init defs vid = Hashtbl.add defs vid [ [], IsInit ] *) (**************************************************************) (* Convert from Lustre expressions to Z3 expressions and back *) @@ -33,24 +34,27 @@ let pp_hash pp_key pp_v fmt h = (fun key v -> Format.fprintf fmt "%a -> %a@ " pp_key key pp_v v) h -let pp_e_map fmt = - List.iter - (fun (e, t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) - !expr_hash - -let pp_ze_hash fmt = - pp_hash - (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)) - Format.pp_print_int - fmt - ze_hash - -let pp_e_hash fmt = - pp_hash - Format.pp_print_int - (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)) - fmt - e_hash +(* XXX: UNUSED *) +(* let pp_e_map fmt = *) +(* List.iter *) +(* (fun (e, t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) *) +(* !expr_hash *) + +(* XXX: UNUSED *) +(* let pp_ze_hash fmt = *) +(* pp_hash *) +(* (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)) *) +(* Format.pp_print_int *) +(* fmt *) +(* ze_hash *) + +(* XXX: UNUSED *) +(* let pp_e_hash fmt = *) +(* pp_hash *) +(* Format.pp_print_int *) +(* (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e)) *) +(* fmt *) +(* e_hash *) let mem_expr e = (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]" diff --git a/src/tools/stateflow/common/datatype.ml b/src/tools/stateflow/common/datatype.ml index ab8985985930635d9cff7699336216e847f6a89b..a84c88647fd500add56bcdd7165ec7412f83cb3b 100644 --- a/src/tools/stateflow/common/datatype.ml +++ b/src/tools/stateflow/common/datatype.ml @@ -206,28 +206,30 @@ module SF = struct Printers.pp_var fmt globvar.GlobalVarDef.variable)) src - let pp_prog fmt (Program (name, component_list, vars)) = - Format.fprintf - fmt - "Main node name: %s@ %a@ %a@" - name - (pp_src pp_sffunction) - component_list - pp_vars - vars + (* XXX: UNUSED *) + (* let pp_prog fmt (Program (name, component_list, vars)) = *) + (* Format.fprintf *) + (* fmt *) + (* "Main node name: %s@ %a@ %a@" *) + (* name *) + (* (pp_src pp_sffunction) *) + (* component_list *) + (* pp_vars *) + (* vars *) - let pp_scope fmt src = - Format.fprintf - fmt - (match src with - | Constant -> - "Constant" - | Input -> - "Input" - | Local -> - "Local" - | Output -> - "Output" - | Parameter -> - "Parameter") + (* XXX: UNUSED *) + (* let pp_scope fmt src = *) + (* Format.fprintf *) + (* fmt *) + (* (match src with *) + (* | Constant -> *) + (* "Constant" *) + (* | Input -> *) + (* "Input" *) + (* | Local -> *) + (* "Local" *) + (* | Output -> *) + (* "Output" *) + (* | Parameter -> *) + (* "Parameter") *) end diff --git a/src/tools/zustre/zustre_common.ml b/src/tools/zustre/zustre_common.ml index 4201a749dc0f1dac0b1e6dc2523ff4b26415b112..45744a93e04c4056840a60b3a781b9e4e8b09476 100644 --- a/src/tools/zustre/zustre_common.ml +++ b/src/tools/zustre/zustre_common.ml @@ -115,12 +115,13 @@ let get_fdecl id = Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found -let pp_fdecls fmt = - Format.fprintf - fmt - "Registered fdecls: @[%a@]@ " - (Utils.Format.pp_print_list Format.pp_print_string) - (Hashtbl.fold (fun id _ accu -> id :: accu) decls []) +(* XXX: UNUSED *) +(* let pp_fdecls fmt = *) +(* Format.fprintf *) +(* fmt *) +(* "Registered fdecls: @[%a@]@ " *) +(* (Utils.Format.pp_print_list Format.pp_print_string) *) +(* (Hashtbl.fold (fun id _ accu -> id :: accu) decls []) *) let decl_var id = (* Format.eprintf "Declaring var %s@." id.var_id; *) @@ -182,11 +183,14 @@ let decl_rel ?(no_additional_vars = false) name args_sorts = (* Shared variables to describe counter and uid *) let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int -let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) + +(* XXX: UNUSED *) +(* let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) *) let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort let _ = register_fdecl "__uid__" uid_fd -let uid_var = Z3.Expr.mk_const_f !ctx uid_fd +(* XXX: UNUSED *) +(* let uid_var = Z3.Expr.mk_const_f !ctx uid_fd *) (** Conversion functions @@ -412,25 +416,26 @@ let no_reset_to_exprs machines m i = in exprs -let instance_reset_to_exprs machines m i = - let n, _ = List.assoc i m.minstances in - let target_machine = - List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines - in - let vars = - rename_machine_list - (concat m.mname.node_id i) - (rename_current_list (full_memory_vars machines target_machine)) - @ rename_mid_list (full_memory_vars machines target_machine) - in - - let expr = - Z3.Expr.mk_app - !ctx - (get_fdecl (machine_reset_name (Corelang.node_name n))) - (List.map horn_var_to_expr (idx :: uid :: vars)) - in - [ expr ] +(* XXX: UNUSED *) +(* let instance_reset_to_exprs machines m i = *) +(* let n, _ = List.assoc i m.minstances in *) +(* let target_machine = *) +(* List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines *) +(* in *) +(* let vars = *) +(* rename_machine_list *) +(* (concat m.mname.node_id i) *) +(* (rename_current_list (full_memory_vars machines target_machine)) *) +(* @ rename_mid_list (full_memory_vars machines target_machine) *) +(* in *) + +(* let expr = *) +(* Z3.Expr.mk_app *) +(* !ctx *) +(* (get_fdecl (machine_reset_name (Corelang.node_name n))) *) +(* (List.map horn_var_to_expr (idx :: uid :: vars)) *) +(* in *) +(* [ expr ] *) let instance_call_to_exprs machines reset_instances m i inputs outputs = let self = m.mname.node_id in diff --git a/src/utils/utils.ml b/src/utils/utils.ml index dc11588056670dc36cf8c469cd5ab2a725776d09..204929c0bf0d277d970c468698fb089243f7dbc9 100644 --- a/src/utils/utils.ml +++ b/src/utils/utils.ml @@ -414,21 +414,22 @@ let new_tag = module List = struct include List - let iteri2 f l1 l2 = - if List.length l1 <> List.length l2 then - raise (Invalid_argument "iteri2: lists have different lengths") - else - let rec run idx l1 l2 = - match l1, l2 with - | [], [] -> - () - | hd1 :: tl1, hd2 :: tl2 -> - f idx hd1 hd2; - run (idx + 1) tl1 tl2 - | _ -> - assert false - in - run 0 l1 l2 + (* XXX: UNUSED *) + (* let iteri2 f l1 l2 = *) + (* if List.length l1 <> List.length l2 then *) + (* raise (Invalid_argument "iteri2: lists have different lengths") *) + (* else *) + (* let rec run idx l1 l2 = *) + (* match l1, l2 with *) + (* | [], [] -> *) + (* () *) + (* | hd1 :: tl1, hd2 :: tl2 -> *) + (* f idx hd1 hd2; *) + (* run (idx + 1) tl1 tl2 *) + (* | _ -> *) + (* assert false *) + (* in *) + (* run 0 l1 l2 *) let rec extract l fst last = if last < fst then assert false diff --git a/tests b/tests index e105387a286411191249cf52040e1f0195ba3ac6..0c21dcf2be00b55f34c1ccc569be723af1f8dc2e 160000 --- a/tests +++ b/tests @@ -1 +1 @@ -Subproject commit e105387a286411191249cf52040e1f0195ba3ac6 +Subproject commit 0c21dcf2be00b55f34c1ccc569be723af1f8dc2e