From a4ba5576b9ef34ddc1e00ea4836ca50decde05b5 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Mon, 25 Mar 2024 17:41:06 +0100
Subject: [PATCH] [wp] Extracting logic type info parameters from Tysymbol
---
src/plugins/wp/Why3Import.ml | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 18a301c825c..405b42906ec 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -79,12 +79,15 @@ let rec _lt_of_ts (ty : W.Ty.ty) =
| W.Ty.Tyapp (tys,tyl) ->
L.debug ~level:0 "Tysymbol %a.@" pp_id tys.ts_name;
L.debug ~level:0 "Tysymbol location %a.@" pp_id_loc tys.ts_name;
+ (*lti_of_ls (?)*)
List.iter (fun ty -> _lt_of_ts ty ) tyl;
(* Cil_types.Lreal *)
and _lti_of_ls (tys : W.Ty.tysymbol) : Cil_types.logic_type_info =
{
lt_name = tys.ts_name.id_string;
- lt_params = [""];
+ lt_params = List.map (fun (tvs : W.Ty.tvsymbol )->
+ tvs.tv_name.id_string
+ ) tys.ts_args;
lt_def = None;
lt_attr = [];
}
--
GitLab