From 8330d9d62e52a8ff576b510a0dae87e4d5305cf3 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Mon, 8 Nov 2021 16:07:05 +0100
Subject: [PATCH] [e-acsl] change optional argument to mandatory
---
src/plugins/e-acsl/src/analyses/typing.ml | 26 ++++++++++---------
src/plugins/e-acsl/src/analyses/typing.mli | 6 ++---
.../src/code_generator/at_with_lscope.ml | 14 +++++++---
src/plugins/e-acsl/src/code_generator/libc.ml | 4 +--
.../src/code_generator/memory_translate.ml | 8 ++++--
.../e-acsl/src/code_generator/translate.ml | 6 ++---
6 files changed, 39 insertions(+), 25 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index e1e24001f37..e4d122b5ed6 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -194,11 +194,11 @@ module Id_term_with_lenv =
info is already computed for a term, it is never recomputed *)
module Memo: sig
val memo:
- ?lenv:Function_params_ty.t ->
+ lenv:Function_params_ty.t ->
(term -> computed_info) ->
term ->
computed_info Error.or_error
- val get: ?lenv:Function_params_ty.t -> term ->
+ val get: lenv:Function_params_ty.t -> term ->
computed_info Error.or_error
val clear: unit -> unit
end = struct
@@ -241,7 +241,7 @@ end = struct
try Misc.Id_term.Hashtbl.find tbl t
with Not_found -> Error.not_memoized ()
- let get ?(lenv=[]) t =
+ let get ~lenv t =
match lenv with
| [] -> get_nondep t
| _::_ -> get_dep lenv t
@@ -267,7 +267,7 @@ end = struct
Id_term_with_lenv.Hashtbl.add dep_tbl (t, lenv) x;
x
- let memo ?(lenv=[]) f t =
+ let memo ~lenv f t =
match lenv with
| [] -> memo_nondep f t
| _::_ -> memo_dep f t lenv
@@ -390,7 +390,7 @@ let rec type_term
?(under_lambda=false)
?(arith_operand=false)
?ctx
- ?(lenv=[])
+ ~lenv
t =
let ctx = Option.map (mk_ctx ~use_gmp_opt) ctx in
let dup ty = ty, ty in
@@ -667,7 +667,7 @@ let rec type_term
ignore (type_term ~use_gmp_opt:true ~lenv li_t);
dup (type_term ~use_gmp_opt:true ?ctx ~lenv t).ty
| Tlambda ([ _ ],lt) ->
- dup (type_term ~use_gmp_opt:true ~under_lambda:true ?ctx lt).ty;
+ dup (type_term ~use_gmp_opt:true ~under_lambda:true ?ctx ~lenv lt).ty;
| Tlambda (_,_) -> Error.not_yet "lambda"
| TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"
@@ -810,7 +810,7 @@ and type_bound_variables ~loc ~lenv (t1, lv, t2) =
Interval.Env.add lv i;
(t1, lv, t2)
-and type_predicate ?(lenv=[]) p =
+and type_predicate ~lenv p =
match Logic_normalizer.get_pred p with
| PoT_term t -> type_term ~use_gmp_opt:true ~lenv t
| PoT_pred p ->
@@ -893,7 +893,9 @@ and type_predicate ?(lenv=[]) p =
end
| Pseparated tlist ->
List.iter
- (fun t -> ignore (type_term ~use_gmp_opt:false ~ctx:Nan t))
+ (fun t ->
+ ignore
+ (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t))
tlist;
c_int
| Pinitialized(_, t)
@@ -903,14 +905,14 @@ and type_predicate ?(lenv=[]) p =
| Pvalid_read(_, t)
| Pobject_pointer(_,t)
| Pvalid_function t ->
- ignore (type_term ~use_gmp_opt:false ~ctx:Nan t);
+ ignore (type_term ~use_gmp_opt:false ~ctx:Nan ~lenv t);
c_int
| Pat(p, _) -> (type_predicate ~lenv p).ty
| Pfresh _ -> Error.not_yet "\\fresh"
in
coerce ~arith_operand:false ~ctx:c_int ~op c_int
-let type_term ~use_gmp_opt ?ctx ?(lenv=[]) t =
+let type_term ~use_gmp_opt ?ctx ~lenv t =
Options.feedback ~dkey ~level:4 "typing term '%a' in ctx '%a'."
Printer.pp_term t (Pretty_utils.pp_opt D.pretty) ctx;
ignore (type_term ~use_gmp_opt ?ctx ~lenv t);
@@ -918,7 +920,7 @@ let type_term ~use_gmp_opt ?ctx ?(lenv=[]) t =
Stack.pop pending_typing ()
done
-let type_named_predicate ?(lenv=[]) p =
+let type_named_predicate ~lenv p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
Printer.pp_predicate p;
ignore (type_predicate ~lenv p);
@@ -926,7 +928,7 @@ let type_named_predicate ?(lenv=[]) p =
Stack.pop pending_typing ()
done
-let unsafe_set t ?ctx ?(lenv=[]) ty =
+let unsafe_set t ?ctx ~lenv ty =
let ctx = match ctx with None -> ty | Some ctx -> ctx in
let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
ignore (Memo.memo mk ~lenv t)
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 84e1a12d2af..ae329a3cab1 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -100,14 +100,14 @@ val join: number_ty -> number_ty -> number_ty
val type_term:
use_gmp_opt:bool ->
?ctx:number_ty ->
- ?lenv:Function_params_ty.t ->
+ lenv:Function_params_ty.t ->
term ->
unit
(** Compute the type of each subterm of the given term in the given context. If
[use_gmp_opt] is false, then the conversion to the given context is done
even if -e-acsl-gmp-only is set. *)
-val type_named_predicate: ?lenv:Function_params_ty.t -> predicate -> unit
+val type_named_predicate: lenv:Function_params_ty.t -> predicate -> unit
(** Compute the type of each term of the given predicate. *)
val clear: unit -> unit
@@ -147,7 +147,7 @@ val get_cast_of_predicate: lenv:Function_params_ty.t -> predicate -> typ option
val unsafe_set:
term ->
?ctx:number_ty ->
- ?lenv:Function_params_ty.t ->
+ lenv:Function_params_ty.t ->
number_ty ->
unit
(** Register that the given term has the given type in the given context (if
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index 43b11a26c74..0171aa913ac 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -171,7 +171,11 @@ let size_from_sizes_and_shifts ~loc = function
(* Build the left-value corresponding to [*(at + index)]. *)
let lval_at_index ~loc kf env (e_at, vi_at, t_index) =
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int t_index;
+ Typing.type_term
+ ~use_gmp_opt:false
+ ~ctx:Typing.c_int
+ ~lenv:(Env.Local_vars.get env)
+ t_index;
let term_to_exp = !term_to_exp_ref in
let e_index, _, env = term_to_exp ~adata:Assert.no_data kf env t_index in
let e_index = Cil.constFold false e_index in
@@ -265,8 +269,12 @@ let to_exp ~loc kf env pot label =
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
- Typing.type_term ~use_gmp_opt:false t_size;
- let malloc_stmt = match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t_size with
+ Typing.type_term
+ ~use_gmp_opt:false
+ ~lenv:(Env.Local_vars.get env)
+ t_size;
+ let malloc_stmt =
+ match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t_size with
| Typing.C_integer IInt ->
let e_size, _, _ =
term_to_exp ~adata:Assert.no_data kf env t_size
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 16baa65d7de..1567ea882fa 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -25,7 +25,7 @@
open Cil_types
(* Retrieve the name of the caller function. [vorig_name] is used instead of
- [vname] because some plugins like "Variadic" may change the value of [vname]Â
+ [vname] because some plugins like "Variadic" may change the value of [vname]
for some functions like [sprintf]. *)
let get_caller_name caller =
caller.vorig_name
@@ -187,7 +187,7 @@ let check_integer_bounds ~from target =
If [check_lower_bound] is set to false, then the lower bound check is not
performed. *)
let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
- Typing.type_term ~use_gmp_opt:false t;
+ Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) t;
match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
| Typing.Gmpz ->
let e, _, env =
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index d92926c8163..3698c7cd8db 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -212,7 +212,11 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
(Ctype typ_charptr)
in
- Typing.type_term ~use_gmp_opt:false ~ctx:Typing.nan ptr;
+ Typing.type_term
+ ~use_gmp_opt:false
+ ~ctx:Typing.nan
+ ~lenv:(Env.Local_vars.get env)
+ ptr;
let (ptr, adata), env =
Env.with_rte_and_result env true
~f:(fun env ->
@@ -260,7 +264,7 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
in
Logic_const.term ~loc (Tlet (size_term_info, size_term_if)) Linteger
in
- Typing.type_term ~use_gmp_opt:false size_term;
+ Typing.type_term ~use_gmp_opt:false ~lenv:(Env.Local_vars.get env) size_term;
let size, adata, env =
match Typing.get_number_ty size_term ~lenv:(Env.Local_vars.get env) with
| Typing.Gmpz ->
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2f359ead172..5ccbd1f80ed 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -1386,7 +1386,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
pred_name = pred_name :: lower_guard_pp.pred_name }
in
let lower_guard = Logic_const.prel ~loc (Rge, t, zero_term) in
- Typing.type_named_predicate lower_guard;
+ Typing.type_named_predicate ~lenv:(Env.Local_vars.get env) lower_guard;
let adata_lower_guard, env = Assert.empty ~loc kf env in
let lower_guard, adata_lower_guard, env =
predicate_to_exp ~adata:adata_lower_guard kf env lower_guard
@@ -1416,7 +1416,7 @@ let gmp_to_sizet ~adata ~loc ~name ?(check_lower_bound=true) ?pp kf env t =
pred_name = pred_name :: upper_guard_pp.pred_name }
in
let upper_guard = Logic_const.prel ~loc (Rle, t, sizet_max) in
- Typing.type_named_predicate upper_guard;
+ Typing.type_named_predicate ~lenv:(Env.Local_vars.get env) upper_guard;
let adata_upper_guard, env = Assert.empty ~loc kf env in
let upper_guard, adata_upper_guard, env =
predicate_to_exp ~adata:adata_upper_guard kf env upper_guard
@@ -1500,7 +1500,7 @@ let untyped_term_to_exp typ t =
| _ -> Typing.nan
in
let ctx = Option.map ctx_of_typ typ in
- Typing.type_term ~use_gmp_opt:true ?ctx t;
+ Typing.type_term ~use_gmp_opt:true ~lenv:[] ?ctx t;
let env = Env.push Env.empty in
let env = Env.rte env false in
let e, _, env =
--
GitLab