From 118e9c5c55ccf27c27c88909bfd5dcc20f973b60 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <erwan.jahier@univ-grenoble-alpes.fr>
Date: Tue, 27 Feb 2024 16:58:21 +0100
Subject: [PATCH] add a kind2 comment for the main node if --assert-in-contract
is used
---
lib/licDump.ml | 10 +++++++---
lib/licPrg.ml | 7 ++++---
2 files changed, 11 insertions(+), 6 deletions(-)
diff --git a/lib/licDump.ml b/lib/licDump.ml
index e22b8cb..1b9a816 100644
--- a/lib/licDump.ml
+++ b/lib/licDump.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/02/2024 (at 17:54) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/02/2024 (at 16:20) by Erwan Jahier> *)
(*
This module is used both for
@@ -834,7 +834,7 @@ and (const_decl: bool -> Lv6Id.long -> Lic.const -> string) =
)
(* exported *)
-and node_of_node_exp_eff forprint (neff: Lic.node_exp): string =
+and node_of_node_exp_eff is_main_node forprint (neff: Lic.node_exp): string =
wrap_long_profile (
(
if neff.is_safe_eff then "" else "unsafe "
@@ -886,7 +886,11 @@ and node_of_node_exp_eff forprint (neff: Lic.node_exp): string =
("var\n " ^ (string_of_type_decl_list forprint l ";\n ") ^ ";\n")
)
^ (if global_opt.assert_in_contract then
- Printf.sprintf "let\n %s" eqs_str
+ Printf.sprintf "let\n %s%s" eqs_str
+ (if is_main_node then "
+--%MAIN ;
+--%PROPERTY "^ (List.hd neff.outlist_eff).var_name_eff ^";
+" else "")
else
("let\n " ^ ass_str ^ eqs_str)
) ^
diff --git a/lib/licPrg.ml b/lib/licPrg.ml
index 4fcf5e0..7e09a05 100644
--- a/lib/licPrg.ml
+++ b/lib/licPrg.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 08/06/2023 (at 10:49) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/02/2024 (at 15:56) by Erwan Jahier> *)
open Lv6MainArgs
module ItemKeyMap = struct
@@ -307,7 +307,7 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
Hence we print the first one (if no main node is set).
*)
let nexp = get_main_node_exp this main_node in
- output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff true nexp);
+ output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff true true nexp);
flush opt.Lv6MainArgs.oc;
) else (
(* Pour les noeuds, pas sur que ça marche tant qu'on n'a
@@ -320,12 +320,13 @@ let to_file (opt: Lv6MainArgs.t) (this:t) (main_node: Lv6Id.idref option) =
On n'affiche PAS les extern Lustre::...
*)
+ let nexp_main = get_main_node_exp this main_node in
NodeKeyMap.iter (
fun _ nexp ->
match nexp.Lic.node_key_eff with
(* inutile d'écrire les noeuds predefs *)
| (("Lustre",_),[]) -> ()
- | _ -> output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff true nexp)
+ | _ -> output_string opt.Lv6MainArgs.oc (LicDump.node_of_node_exp_eff (nexp_main = nexp) true nexp)
)
this.nodes
)
--
GitLab