[wp] rename tau_of_li_type into tau_of_return

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

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

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 ;