From 875b043ee920cbc3e2551874ace97140a7c70306 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Mon, 13 May 2024 13:49:03 +0200
Subject: [PATCH] [wp] Printing functions parameters, additionnal debug info at
level 2/3
---
src/plugins/wp/Why3Import.ml | 22 +++++++++++++++++-----
1 file changed, 17 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index b936c201077..d4d681572d6 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -92,9 +92,15 @@ let pp_lti fmt (lti : C.logic_type_info) =
let pp_li fmt (li : C.logic_info) =
Cpp.pp_logic_info fmt li
-(* -------------------------------------------------------------------------- *)
-(* --- Types --- *)
-(* -------------------------------------------------------------------------- *)
+(* For debug only*)
+let pp_lvs fmt (lvs : C.logic_var list) =
+ List.iter (fun (lv: C.logic_var) -> Cpp.pp_logic_var fmt lv;
+ Cpp.pp_logic_type fmt lv.lv_type)
+ lvs;
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Types --- *)
+ (* -------------------------------------------------------------------------- *)
type tenv = C.logic_type_info W.Ty.Hts.t
type lenv = C.logic_info W.Term.Hls.t
@@ -114,10 +120,15 @@ let _populate_tenv_builtin (tenv:tenv) =
(* -------------------------------------------------------------------------- *)
let tvars_of_txs (txs: W.Ty.tvsymbol list) : string list * tvars =
+ L.debug ~level:3 "Called tvars_of_txs";
+ List.iter (fun (tv: W.Ty.tvsymbol) ->
+ L.debug ~level:3 "Name of : %a" pp_id tv.tv_name) txs;
List.fold_right
(fun (tv: W.Ty.tvsymbol) (txs,tvs) ->
let x = tv.tv_name.id_string in
- x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
+ match x with
+ | "int" -> x :: txs, W.Ty.Mtv.add tv (C.Linteger) tvs
+ | _ -> x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
) txs ([], W.Ty.Mtv.empty)
@@ -241,7 +252,8 @@ let () =
) tenv;
W.Term.Hls.iter (fun (ls) (li) ->
L.debug ~level:1 "Why3 logic symbol : %a" pp_ls ls;
- L.debug ~level:1 "Corresponding CIL logic info %a" pp_li li;
+ L.debug ~level:1 "Corresponding CIL logic info : %a" pp_li li;
+ L.debug ~level:1 "Associated parameters : %a" pp_lvs li.l_profile;
) lenv
end
--
GitLab