From f57127eea37e6a968a31e5ff89762520aaebbfe5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 30 Mar 2023 16:53:59 +0200
Subject: [PATCH] [wp] rename tau_of_li_type into tau_of_return
---
src/plugins/wp/Lang.ml | 7 ++-----
src/plugins/wp/Lang.mli | 2 +-
src/plugins/wp/LogicCompiler.ml | 6 +++---
3 files changed, 6 insertions(+), 9 deletions(-)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 91272859fed..5721069a037 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -225,10 +225,7 @@ let rec tau_of_ltype t =
| Ltype _ as b when Logic_const.is_boolean_type b -> Logic.Bool
| Ltype(lt,lts) -> atype lt (List.map tau_of_ltype lts)
-let tau_of_li_type ltype =
- match ltype with
- | None -> Logic.Prop
- | Some t -> tau_of_ltype t
+let tau_of_return = function None -> Logic.Prop | Some t -> tau_of_ltype t
(* -------------------------------------------------------------------------- *)
(* --- Datatypes --- *)
@@ -420,7 +417,7 @@ and source =
let tau_of_lfun phi ts =
match phi with
- | ACSL f -> tau_of_li_type f.l_type
+ | ACSL f -> tau_of_return f.l_type
| CTOR c ->
if c.ctor_type.lt_params = [] then Logic.Data(Atype c.ctor_type,[])
else raise Not_found
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 4c196d1fa5e..0dbdfa312a7 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -158,7 +158,7 @@ val extern_t:
val tau_of_object : c_object -> tau
val tau_of_ctype : typ -> tau
val tau_of_ltype : logic_type -> tau
-val tau_of_li_type : logic_type option -> tau
+val tau_of_return : logic_type option -> tau
val tau_of_lfun : lfun -> tau option list -> tau
val tau_of_field : field -> tau
val tau_of_record : field -> tau
diff --git a/src/plugins/wp/LogicCompiler.ml b/src/plugins/wp/LogicCompiler.ml
index 34148ea3695..ffb93c239c4 100644
--- a/src/plugins/wp/LogicCompiler.ml
+++ b/src/plugins/wp/LogicCompiler.ml
@@ -440,7 +440,7 @@ struct
let frame = logic_frame name types in
in_frame frame
begin fun () ->
- let tres = Lang.tau_of_li_type tres in
+ let tres = Lang.tau_of_return tres in
let env,domain,sigv = profile_env Logic_var.Map.empty [] [] profile in
let env = default_label env labels in
let result = cc env data in
@@ -563,7 +563,7 @@ struct
in_frame frame
begin fun () ->
let lfun = ACSL l in
- let tau = Lang.tau_of_li_type l.l_type in
+ let tau = Lang.tau_of_return l.l_type in
let parp,sigp = Lang.local profile_sig l.l_profile in
let ldef = {
d_lfun = lfun ;
@@ -586,7 +586,7 @@ struct
in_frame frame
begin fun () ->
let lfun = ACSL l in
- let tau = Lang.tau_of_li_type l.l_type in
+ let tau = Lang.tau_of_return l.l_type in
let parm,sigm = Lang.local (profile_mem l) vars in
let ldef = {
d_lfun = lfun ;
--
GitLab