From 2d7bfedd9cb6bc0f5f7f3ea872a394891344d5c5 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Mon, 25 Mar 2024 11:19:25 +0100
Subject: [PATCH] [wp] Stub for creation of logic_type_info
---
src/plugins/wp/Why3Import.ml | 30 +++++++++++++++++++++++++++---
1 file changed, 27 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index f1c18ab4f6e..94510191ebd 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -42,10 +42,34 @@ let extract_path thname =
let pp_id fmt (id: W.Ident.ident) =
Format.pp_print_string fmt id.id_string
-let rec lt_of_ts : W.Ty.ty -> Cil_types.logic_type =
- raise Not_found
-and lti_of_ls : W.Ty.tysymbol -> Cil_types.logic_type_info =
+(* logic_type =
+ | Ctype of typ (** a C type *)
+ | Ltype of logic_type_info * logic_type list
+ (** an user-defined logic type with its parameters *)
+ | Lvar of string (** a type variable. *)
+ | Linteger (** mathematical integers, {i i.e.} Z *)
+ | Lreal (** mathematical reals, {i i.e.} R *)
+ | Larrow of logic_type list * logic_type (** (n-ary) function type *)*)
+
+(*logic_type_info = {
+ mutable lt_name: string;
+ lt_params : string list; (** type parameters*)
+ mutable lt_def: logic_type_def option;
+ (** definition of the type. None for abstract types. *)
+ mutable lt_attr: attributes;
+ (** attributes associated to the logic type.
+ @since Phosphorus-20170501-beta1 *)
+}*)
+
+let rec lt_of_ts (_ty : W.Ty.ty) : Cil_types.logic_type =
raise Not_found
+and lti_of_ls (tys : W.Ty.tysymbol) : Cil_types.logic_type_info =
+ {
+ lt_name = tys.ts_name.id_string;
+ lt_params = [""];
+ lt_def = None;
+ lt_attr = [];
+ }
let import_theory env thname =
let theory_name, theory_path = extract_path thname in
--
GitLab