From 6d1237554b84cbd8e789ddb72c9b1eacb96a593c Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Thu, 16 May 2024 17:47:48 +0200
Subject: [PATCH] [wp] Added why3module definition for module-scoped envs
---
src/plugins/wp/Why3Import.ml | 18 +++++++-----------
1 file changed, 7 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index d5d05ab2aa0..9890a6cedee 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -105,13 +105,19 @@ let pp_lvs fmt (lvs : C.logic_var list) =
type tvars = C.logic_type W.Ty.Mtv.t
+type why3module = {
+ paths : string list;
+ types : C.logic_type_info list;
+ logics : C.logic_info list;
+}
+
type env = {
wenv : W.Env.env;
tenv : C.logic_type_info W.Ty.Hts.t;
lenv : C.logic_info W.Term.Hls.t;
lils : W.Term.lsymbol Logic_info.Hashtbl.t;
ltits : W.Ty.tysymbol Logic_type_info.Hashtbl.t;
- _menv : (list C.global_annotation) Datatype.String.Hashtbl.t
+ _menv : why3module Datatype.String.Hashtbl.t
}
@@ -178,16 +184,6 @@ and lti_of_ts (env : env) (ts : W.Ty.tysymbol) : C.logic_type_info =
}
in W.Ty.Hts.add env.tenv ts lti ;
Logic_type_info.Hashtbl.add env.ltits lti ts;
- let _gtype : C.typeinfo = C.{
- torig_name = ts.ts_name.id_string;
- }
- (* Datatype.String.Hashtbl.add env._menv (construct_acsl_name ts.ts_name)
- C.GType (
- C.{
- torig_name = ts.ts_name.id_string;
- tname = ts.ts_name.id_string;
- }
- ); *)
lti
--
GitLab