Commit 9f55c7a6 authored by Julien Signoles's avatar Julien Signoles
Browse files

[Env] renaming + simplification in Env.Logic_binding

parent 62de7356
......@@ -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
......
......@@ -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. *)
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment