From 4e22745004f52206695cff4f1ee0e9536a1f2d32 Mon Sep 17 00:00:00 2001 From: Rob Lorch Date: Mon, 29 Jul 2024 19:02:52 -0400 Subject: [PATCH] Fix bug when checking realizability but not environment --- src/lustre/lustreInput.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/src/lustre/lustreInput.ml b/src/lustre/lustreInput.ml index 5efe09bb7..804f80ce5 100644 --- a/src/lustre/lustreInput.ml +++ b/src/lustre/lustreInput.ml @@ -333,14 +333,19 @@ let of_channel old_frontend only_parse in_ch = (* If checking realizability, then we are actually checking realizability of Kind 2-generated imported nodes representing the (1) the main node's contract instrumented with type info and - (2) the main node's enviornment *) - if (not main_lustre_node.is_extern) && List.mem `CONTRACTCK (Flags.enabled ()) then - [LustreIdent.mk_string_ident (LGI.contract_tag ^ s); - LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] - else if main_lustre_node.is_extern && List.mem `CONTRACTCK (Flags.enabled ()) then - [s_ident; - LustreIdent.mk_string_ident (LGI.inputs_tag ^ s)] - else [s_ident] + (2) the main node's enviornment, if environment checking is enabled *) + let main_nodes = + if (not main_lustre_node.is_extern) && List.mem `CONTRACTCK (Flags.enabled ()) then + [LustreIdent.mk_string_ident (LGI.contract_tag ^ s);] + else [s_ident] + in + let main_nodes = + if (Flags.Contracts.check_environment ()) && List.mem `CONTRACTCK (Flags.enabled ()) then + LustreIdent.mk_string_ident (LGI.inputs_tag ^ s) :: main_nodes + else + main_nodes + in + main_nodes (* User-specified main node in command-line input might not exist *) with Not_found -> let msg =