From 9f55c7a6a77f5db9817bafae4b58aaeedaf125cc Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 1 Mar 2019 08:57:20 +0100
Subject: [PATCH] [Env] renaming + simplification in Env.Logic_binding
---
src/plugins/e-acsl/env.ml | 53 +++++++++++----------------
src/plugins/e-acsl/env.mli | 5 ++-
src/plugins/e-acsl/logic_functions.ml | 2 +-
3 files changed, 25 insertions(+), 35 deletions(-)
diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index a1e2b5d26c4..e987bd4f613 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -279,19 +279,30 @@ let new_var_and_mpz_init ~loc ?scope ?name env t mk_stmts =
module Logic_binding = struct
+ let add_binding env logic_v vi =
+ try
+ let varinfos = Logic_var.Map.find logic_v env.var_mapping in
+ Stack.push vi varinfos;
+ env
+ with Not_found | Stack.Empty ->
+ let varinfos = Stack.create () in
+ Stack.push vi varinfos;
+ let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
+ { env with var_mapping = var_mapping }
+
let add ?ty env logic_v =
let ty = match ty with
| Some ty -> ty
| None -> match logic_v.lv_type with
- | Ctype ty -> ty
- | Linteger -> Gmpz.t ()
- | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
- | Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
- let msg =
- Format.asprintf
- "logic variable of type %a" Logic_type.pretty lty
- in
- Error.not_yet msg
+ | Ctype ty -> ty
+ | Linteger -> Gmpz.t ()
+ | Ltype _ as ty when Logic_const.is_boolean_type ty -> Cil.charType
+ | Ltype _ | Lvar _ | Lreal | Larrow _ as lty ->
+ let msg =
+ Format.asprintf
+ "logic variable of type %a" Logic_type.pretty lty
+ in
+ Error.not_yet msg
in
let v, e, env = new_var
~loc:Location.unknown
@@ -301,29 +312,7 @@ module Logic_binding = struct
ty
(fun _ _ -> [])
in
- let env =
- try
- let varinfos = Logic_var.Map.find logic_v env.var_mapping in
- Stack.push v varinfos;
- env
- with Not_found ->
- let varinfos = Stack.create () in
- Stack.push v varinfos;
- let var_mapping = Logic_var.Map.add logic_v varinfos env.var_mapping in
- { env with var_mapping = var_mapping }
- in
- v, e, env
-
- let add_existing_vi env lv vi =
- try
- let varinfos = Logic_var.Map.find lv env.var_mapping in
- Stack.push vi varinfos;
- env
- with Not_found | Stack.Empty ->
- let varinfos = Stack.create () in
- Stack.push vi varinfos;
- let var_mapping = Logic_var.Map.add lv varinfos env.var_mapping in
- { env with var_mapping = var_mapping }
+ v, e, add_binding env logic_v v
let get env logic_v =
try
diff --git a/src/plugins/e-acsl/env.mli b/src/plugins/e-acsl/env.mli
index 1339e9357f3..abb50cb87e9 100644
--- a/src/plugins/e-acsl/env.mli
+++ b/src/plugins/e-acsl/env.mli
@@ -68,8 +68,9 @@ module Logic_binding: sig
val add: ?ty:typ -> t -> logic_var -> varinfo * exp * t
(* Add a new C binding to the list of bindings for the logic variable. *)
- val add_existing_vi: t -> logic_var -> varinfo -> t
- (* [add_existing_vi env lv vi] defines [vi] as latest C binding for [lv]. *)
+ val add_binding: t -> logic_var -> varinfo -> t
+ (* [add_binding env lv vi] defines [vi] as the latest C binding for
+ [lv]. *)
val get: t -> logic_var -> varinfo
(* Return the latest C binding. *)
diff --git a/src/plugins/e-acsl/logic_functions.ml b/src/plugins/e-acsl/logic_functions.ml
index c5f9d07bf28..11dbf3e154c 100644
--- a/src/plugins/e-acsl/logic_functions.ml
+++ b/src/plugins/e-acsl/logic_functions.ml
@@ -185,7 +185,7 @@ let add_varinfo_bindings ~loc kf env lfs =
match Typing.ty_of_logic_ty lty with
| Typing.C_type _ | Typing.Other ->
(* Case A *)
- Env.Logic_binding.add_existing_vi env lv vi_arg
+ Env.Logic_binding.add_binding env lv vi_arg
| Typing.Gmp ->
(* Case B *)
let ty = Typing.typ_of_lty lv.lv_type in
--
GitLab