diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index ed0cbcbfc148a04e8ac97f7a73dab1e05163ca7d..9eb2aadfb3e4a3b60af18a50fb6f73e974729f09 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -77,7 +77,7 @@ CODE_GENERATOR_CMI:=$(addprefix src/code_generator/, $(CODE_GENERATOR_CMI))
SRC_CODE_GENERATOR:= \
smart_exp \
smart_stmt \
- smart_term \
+ smart_term \
gmp \
label \
env \
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 205843023a04fff19017f117e6fae158248202bc..29c06ad7948487084f319c467bfd9f4b0a6bb516 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -675,7 +675,8 @@ and infer_term_host thost =
let infer t =
let i = infer t in
- Logic_function_env.clear(); i
+ Logic_function_env.clear();
+ i
include D
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli b/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
index 2a15a4e582347df4cc465f831f104529480c4645..016b6ed427a86bfadd204aaf466a16a558266862 100644
--- a/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
+++ b/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
@@ -22,10 +22,24 @@
open Cil_types
+(** This module is dedicated to some preprocessing on the predicates
+ - It guards all the [Pvalid] and [Pvalid_read] clauses with
+ an adequate [Pinitialized] clause
+ - It replaces all the applications [Papp] by a corresponding
+ term obtained as an application [Tapp]
+ The predicates that have undergone these changed are
+ called the preprocessed predicates.
+*)
+
val preprocess : file -> unit
+(** Preprocess all the predicates of the ast and store the results *)
val preprocess_annot : code_annotation -> unit
+(** Preprocess of the predicate of a single code annotation and store
+ the results *)
val preprocess_predicate : predicate -> unit
+(** Preprocess a predicate and its children and store the results *)
val get_preprocessed_form : predicate -> Lscope.pred_or_term
+(** Retrieve the preprocessed form of a predicate *)
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
index 3fbe5e5ac6bb6cac2a9846deeb6c1f36134bff37..d4292aa3f6b4b1002e900c89423407daeb958e81 100644
--- a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
+++ b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
@@ -22,9 +22,10 @@
open Cil_types
-let must_translate_ref : (Property.t -> bool) ref =
+let must_translate_ref: (Property.t -> bool) ref =
Extlib.mk_fun "must_translate_ref"
-let must_translate_opt_ref : (Property.t option -> bool) ref =
+
+let must_translate_opt_ref: (Property.t option -> bool) ref =
Extlib.mk_fun "must_translate_opt_ref"
let type_requires v kf kinstr bhvr =
@@ -48,7 +49,6 @@ let type_requires v kf kinstr bhvr =
| Admit -> ())
bhvr.b_requires
-
let type_post_conditions v kf kinstr bhvr =
if Cil.is_default_behavior bhvr then
List.iter
@@ -69,15 +69,13 @@ let type_post_conditions v kf kinstr bhvr =
| Assert | Check -> begin
let post_cond = tp_post_cond.tp_statement in
match termination with
- | Normal ->
- ignore (Visitor.visitFramacPredicate v post_cond)
+ | Normal -> ignore (Visitor.visitFramacPredicate v post_cond)
| Exits | Breaks | Continues | Returns -> ()
end
| Admit -> ())
bhvr.b_post_cond
-
-let typer_visitor (lenv : Typing.Params_ty.t) = object (self)
+let typer_visitor lenv = object (self)
inherit Visitor.frama_c_inplace
(* Only type the globals that do not come from the Rtl *)
@@ -122,9 +120,15 @@ let typer_visitor (lenv : Typing.Params_ty.t) = object (self)
Cil.SkipChildren
method !vspec spec =
- List.iter (fun b -> (List.iter (fun p -> ignore (Visitor.visitFramacIdPredicate self p)) b.b_assumes)) spec.spec_behavior;
- List.iter (type_requires self (Option.get self#current_kf) (self#current_kinstr)) spec.spec_behavior;
- List.iter (type_post_conditions self (Option.get self#current_kf) self#current_kinstr) spec.spec_behavior;
+ List.iter
+ (fun b -> (List.iter (fun p -> ignore (Visitor.visitFramacIdPredicate self p)) b.b_assumes))
+ spec.spec_behavior;
+ List.iter
+ (type_requires self (Option.get self#current_kf) (self#current_kinstr))
+ spec.spec_behavior;
+ List.iter
+ (type_post_conditions self (Option.get self#current_kf) self#current_kinstr)
+ spec.spec_behavior;
Cil.SkipChildren
======= end
=======
@@ -142,7 +146,11 @@ let typer_visitor (lenv : Typing.Params_ty.t) = object (self)
match annot.annot_content with
| AAssert(_, _) | AVariant(_, _) ->
let translate = try
- !must_translate_ref (Property.ip_of_code_annot_single (Option.get self#current_kf) (Option.get self#current_stmt) annot)
+ !must_translate_ref
+ (Property.ip_of_code_annot_single
+ (Option.get self#current_kf)
+ (Option.get self#current_stmt)
+ annot)
with Invalid_argument _ -> true
in
if translate then
@@ -154,7 +162,11 @@ let typer_visitor (lenv : Typing.Params_ty.t) = object (self)
else Cil.DoChildren
| AInvariant(l, _, _) ->
let translate =
- try !must_translate_ref (Property.ip_of_code_annot_single (Option.get self#current_kf) (Option.get self#current_stmt) annot)
+ try !must_translate_ref
+ (Property.ip_of_code_annot_single
+ (Option.get self#current_kf)
+ (Option.get self#current_stmt)
+ annot)
with Invalid_argument _ -> true
in if translate then
if l <> [] then
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.mli b/src/plugins/e-acsl/src/analyses/preprocess_typing.mli
index 61149052044c5e9a0dc3dfbf6fa21c29c9667cae..7d8ee6628e5f4143603c25a3d118b25c276543b0 100644
--- a/src/plugins/e-acsl/src/analyses/preprocess_typing.mli
+++ b/src/plugins/e-acsl/src/analyses/preprocess_typing.mli
@@ -22,14 +22,15 @@
open Cil_types
-val must_translate_ref : (Property.t -> bool) ref
-val must_translate_opt_ref : (Property.t option -> bool) ref
-
-
val type_program : file -> unit
+(** compute and store the type of all the terms that will be translated
+ in a program *)
-(* val type_code_annot : Typing.Params_ty.t -> code_annotation -> unit *)
+val preprocess_predicate : Typing.Function_params_ty.t -> predicate -> unit
+(** compute and store the types of all the terms in a given predicate *)
-val preprocess_predicate : Typing.Params_ty.t -> predicate -> unit
+val preprocess_rte : lenv:Typing.Function_params_ty.t -> code_annotation -> unit
+(** compute and store the type of all the terms in a code annotation *)
-val preprocess_rte : lenv:Typing.Params_ty.t -> code_annotation -> unit
+val must_translate_ref : (Property.t -> bool) ref
+val must_translate_opt_ref : (Property.t option -> bool) ref
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index 23aa1627ba26c46d305e71e43063ed619022409e..163ea8e5a20525976a7df0d19c8dd8672c82d2e6 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -27,8 +27,7 @@ open Cil_types
let dkey = Options.dkey_typing
-let type_subterms : (unit -> unit) Stack.t = Stack.create ()
-
+let stack_type_subterms : (unit -> unit) Stack.t = Stack.create ()
(******************************************************************************)
(** Datatype and constructor *)
@@ -173,16 +172,16 @@ type computed_info =
}
(* Local environement = list of typed variables *)
-module Params_ty =
+module Function_params_ty =
Datatype.List_with_collections
(D)
- (struct let module_name = "E_ACSL.Logic_functions.Params_ty" end)
+ (struct let module_name = "E_ACSL.typing.Function_params_ty" end)
(* Memoization module which retrieves the computed info of some terms. If the
info is already computed for a term, it is never recomputed *)
module Memo: sig
- val memo: ?lenv:Params_ty.t -> (term -> computed_info) -> term -> computed_info
- val get: ?lenv:Params_ty.t -> term -> computed_info
+ val memo: ?lenv:Function_params_ty.t -> (term -> computed_info) -> term -> computed_info
+ val get: ?lenv:Function_params_ty.t -> term -> computed_info
val clear: unit -> unit
end = struct
@@ -206,18 +205,19 @@ end = struct
\\@ logic integer f (integer x) = x + 1;
depends on the type of x. But our type system does not handle dependent types,
which could let us express this dependency natively. Instead, we use the following
- trick to simulate the depedency: We type the corresponding definition (in the example x+1)
+ trick to simulate the dependency: we type the corresponding definition (in the example x+1)
several times, corresponding to the various calls to the function f in the program.
- We distinguish the calls to the function by storing the assocated callstack. *)
- let dep_tbl : computed_info Params_ty.Hashtbl.t Misc.Id_term.Hashtbl.t
+ We distinguish the calls to the function by storing the associated callstack. *)
+ let dep_tbl : computed_info Function_params_ty.Hashtbl.t Misc.Id_term.Hashtbl.t
= Misc.Id_term.Hashtbl.create 97
let get_dep lenv t =
- try let types = Misc.Id_term.Hashtbl.find dep_tbl t in
- Params_ty.Hashtbl.find types lenv
+ try
+ let types = Misc.Id_term.Hashtbl.find dep_tbl t in
+ Function_params_ty.Hashtbl.find types lenv
with Not_found ->
- Options.fatal "[typing] type of term '%a' was never computed with parameters '%a'."
- Printer.pp_term t Params_ty.pretty lenv
+ Options.fatal "[typing] type of term '%a' was never computed with arguments '%a'."
+ Printer.pp_term t Function_params_ty.pretty lenv
let get_nondep t =
try Misc.Id_term.Hashtbl.find tbl t
@@ -227,8 +227,9 @@ end = struct
Printer.pp_term t
let get ?(lenv=[]) t =
- if (List.compare_length_with lenv 0)==0 then get_nondep t
- else get_dep lenv t
+ match lenv with
+ | [] -> get_nondep t
+ | _::_ -> get_dep lenv t
let memo_nondep f t =
try Misc.Id_term.Hashtbl.find tbl t
@@ -238,23 +239,29 @@ end = struct
x
let memo_dep f t lenv =
- try let types = Misc.Id_term.Hashtbl.find dep_tbl t in
- try Params_ty.Hashtbl.find types lenv
+ try
+ let types = Misc.Id_term.Hashtbl.find dep_tbl t in
+ try Function_params_ty.Hashtbl.find types lenv
with Not_found ->
let ty = f t in
- Params_ty.Hashtbl.add types lenv ty; ty
+ Function_params_ty.Hashtbl.add types lenv ty;
+ ty
with Not_found ->
- let types = Params_ty.Hashtbl.create 97 in
+ let types = Function_params_ty.Hashtbl.create 97 in
let ty = f t in
- Params_ty.Hashtbl.add types lenv ty;
+ Function_params_ty.Hashtbl.add types lenv ty;
Misc.Id_term.Hashtbl.add dep_tbl t types;
ty
let memo ?(lenv=[]) f t =
- if (List.compare_length_with lenv 0)==0 then memo_nondep f t
- else memo_dep f t lenv
+ match lenv with
+ | [] -> memo_nondep f t
+ | _::_ -> memo_dep f t lenv
- let clear () = Options.feedback ~dkey ~level:4 "clearing the table"; Misc.Id_term.Hashtbl.clear tbl
+ let clear () =
+ Options.feedback ~dkey ~level:4 "clearing the typing tables";
+ Misc.Id_term.Hashtbl.clear tbl;
+ Misc.Id_term.Hashtbl.clear dep_tbl
end
@@ -315,7 +322,6 @@ let number_ty_of_typ ~post ty =
| TVoid _ | TPtr _ | TArray _ | TFun _ | TComp _ | TBuiltin_va_list _ -> Nan
| TNamed _ -> assert false
-
let ty_of_logic_ty ?term lty =
let get_ty = function
| Linteger -> Gmpz
@@ -364,8 +370,6 @@ let type_letin li li_t =
(* type the term [t] in a context [ctx] by taking --e-acsl-gmp-only into account
iff [use_gmp_opt] is true. *)
let rec type_term ~use_gmp_opt ?(arith_operand=false) ?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;
let ctx = Option.map (mk_ctx ~use_gmp_opt) ctx in
let dup ty = ty, ty in
let compute_ctx ?ctx i =
@@ -542,11 +546,11 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
(* possible to have an [LBpred] here because we transformed
[Papp] into [Tapp] *)
Stack.push
- (fun _ ->
- let typed_params = type_params ~use_gmp_opt ~lenv li.l_profile args in
+ (fun () ->
+ let typed_params = type_params ~use_gmp_opt ~lenv li.l_profile args li.l_var_info.lv_name in
ignore (type_predicate ~lenv:typed_params p);
List.iter Interval.Env.remove li.l_profile)
- type_subterms;
+ stack_type_subterms;
dup c_int
| LBterm t_body ->
begin match li.l_type with
@@ -555,19 +559,17 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
| Some lty ->
(* TODO: what if the function returns a real? *)
let ty = ty_of_logic_ty ~term:t lty in
- let type_subterm = fun () ->
- let typed_params = type_params ~use_gmp_opt ~lenv li.l_profile args in
+ let type_subterm () =
+ let typed_params = type_params ~use_gmp_opt ~lenv li.l_profile args li.l_var_info.lv_name in
ignore (type_term ~use_gmp_opt ~lenv:typed_params t_body)
in
- let clear_env = fun () ->
- List.iter Interval.Env.remove li.l_profile
- in
+ let clear_env () = List.iter Interval.Env.remove li.l_profile in
Stack.push
clear_env
- type_subterms;
+ stack_type_subterms;
Stack.push
type_subterm
- type_subterms;
+ stack_type_subterms;
dup ty
end
| LBnone ->
@@ -590,14 +592,12 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
ignore (type_term ~use_gmp_opt:true ?ctx ~lenv lambda);
dup ty
| [ ] | [ _ ] | [ _; _ ] | _ :: _ :: _ :: _ ->
- (* Options.fatal "extended quantifier %a is not well formed"
- * Printer.pp_logic_var li.l_var_info *)
Error.not_yet "logic functions or predicates with no definition \
nor reads clause"
+ (* TODO : improve error message to distinguish error messages
+ corresponding to unsupported primitives and wrong application of
+ supported primitive (one is a fatal and the other is a not_yet) *)
)
- (* TODO : improve error message to distinguish error messages
- corresponding to unsupported primitives and wrong application of
- supported primitive (one is a fatal and the other is a not_yet) *)
| LBreads _ ->
Error.not_yet "logic functions or predicates performing read accesses"
| LBinductive _ ->
@@ -625,7 +625,7 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx ?(lenv=[]) t =
| Tlambda ([ _ ],lt) ->
dup (type_term ~use_gmp_opt:true ?ctx lt).ty;
| Tlambda (_,_) -> Error.not_yet "lambda"
- | TDataCons (_,_) ->Error.not_yet "datacons"
+ | TDataCons (_,_) -> Error.not_yet "datacons"
| TUpdate (_,_,_) -> Error.not_yet "update"
| Tnull
@@ -660,20 +660,22 @@ and type_term_offset ~lenv t = match t with
ignore (type_term ~use_gmp_opt:false ~ctx ~lenv t);
type_term_offset ~lenv toff
-and type_params params args ~use_gmp_opt ~lenv =
- try List.fold_right2
- (fun lv t (typed_params : Params_ty.t) ->
- let ty_arg = (type_term ~use_gmp_opt ~lenv t).ty in
- begin
- try
- let typ_arg = typ_of_number_ty ty_arg
- in Interval.Env.add lv (Interval.interv_of_typ typ_arg)
- with Not_a_number -> ()
- end;
- ty_arg :: typed_params)
- params args []
- with Invalid_argument _ -> assert false
-(* TODO : error msg Options.fatal "[Tapp] unexpected number of arguments when calling %s" fname *)
+and type_params params ~use_gmp_opt ~lenv args fname =
+ try
+ List.fold_right2
+ (fun lv t (typed_params : Function_params_ty.t) ->
+ let ty_arg = (type_term ~use_gmp_opt ~lenv t).ty in
+ begin
+ try
+ let typ_arg = typ_of_number_ty ty_arg in
+ Interval.Env.add lv (Interval.interv_of_typ typ_arg)
+ with Not_a_number -> ()
+ end;
+ ty_arg :: typed_params)
+ params
+ args
+ []
+ with Invalid_argument _ -> Options.fatal "[Tapp] unexpected number of arguments when calling %s" fname
(* [type_bound_variables] infers an interval associated with each of
the provided bounds of a quantified variable, and provides a term
@@ -739,7 +741,7 @@ and type_bound_variables ~loc ~lenv (t1, lv, t2) =
let guard_lower = Logic_const.prel ~loc (Rle, guard_lower, lv_term) in
let guard_upper = Logic_const.prel ~loc (Rlt, lv_term, guard_upper) in
let guard = Logic_const.pand ~loc (guard_lower, guard_upper) in
- ignore(type_predicate ~lenv guard);
+ ignore (type_predicate ~lenv guard);
Bound_variables.add_guard_for_small_type lv guard;
t1, t2, i
in
@@ -772,8 +774,8 @@ and type_predicate ?(lenv=[]) p =
begin
match li.l_body with
| LBpred p ->
- let typed_params = type_params ~use_gmp_opt:true ~lenv li.l_profile args in
- ignore(type_predicate ~lenv:typed_params p);
+ let typed_params = type_params ~use_gmp_opt:true ~lenv li.l_profile args li.l_var_info.lv_name in
+ ignore (type_predicate ~lenv:typed_params p);
List.iter Interval.Env.remove li.l_profile
| LBnone -> ()
| LBreads _ -> ()
@@ -819,6 +821,9 @@ and type_predicate ?(lenv=[]) p =
| Pforall _
| Pexists _ -> begin
match Bound_variables.get_preprocessed_quantifier p with
+ (* If there is no preprocessed form for the quantifier, it means that the preprocessing phase
+ raised an error. It is costly to analyze again and determine what was the error, so instead
+ we raise the exception [Ignored] which signifies that no error message should be displayed *)
| None -> Error.ignored ()
| Some (guards, goal) ->
let guards =
@@ -852,20 +857,18 @@ 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);
- while not (Stack.is_empty type_subterms) do
- Stack.pop type_subterms ()
+ while not (Stack.is_empty stack_type_subterms) do
+ Stack.pop stack_type_subterms ()
done
let type_named_predicate ?(lenv=[]) p =
Options.feedback ~dkey ~level:3 "typing predicate '%a'."
Printer.pp_predicate p;
ignore (type_predicate ~lenv p);
- while not (Stack.is_empty type_subterms) do
- Stack.pop type_subterms ()
+ while not (Stack.is_empty stack_type_subterms) do
+ Stack.pop stack_type_subterms ()
done
-
-
let unsafe_set t ?ctx ty =
let ctx = match ctx with None -> ty | Some ctx -> ctx in
let mk _ = coerce ~arith_operand:false ~ctx ~op:ty ty in
@@ -875,10 +878,9 @@ let unsafe_set t ?ctx ty =
(** {2 Getters} *)
(******************************************************************************)
-let get_number_ty t lenv =
- (Memo.get ~lenv t).ty
-let get_integer_op t lenv = (Memo.get ~lenv t).op
-let get_integer_op_of_predicate p lenv = (type_predicate ~lenv p).op
+let get_number_ty ~lenv t = (Memo.get ~lenv t).ty
+let get_integer_op ~lenv t = (Memo.get ~lenv t).op
+let get_integer_op_of_predicate ~lenv p = (type_predicate ~lenv p).op
(* {!typ_of_integer}, but handle the not-integer cases. *)
let extract_typ t ty =
@@ -892,15 +894,15 @@ let extract_typ t ty =
| Lvar _ -> Error.not_yet "unsupported logic type: type variable"
| Larrow _ -> Error.not_yet "unsupported logic type: type arrow"
-let get_typ t lenv =
+let get_typ ~lenv t =
let info = Memo.get ~lenv t in
extract_typ t info.ty
-let get_op t lenv =
+let get_op ~lenv t =
let info = Memo.get ~lenv t in
extract_typ t info.op
-let get_cast t lenv =
+let get_cast ~lenv t =
let info = Memo.get ~lenv t in
try Option.map typ_of_number_ty info.cast
with Not_a_number -> None
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index 2e63eab49dabd309d7ee69d5645e1dd5269c7c41..ac869b8770cb12f32487c5873c0ec4570fb00a49 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -60,9 +60,7 @@ type number_ty = private
| Real
| Nan
-(* module Datatype: Datatype.S_with_collections with type t = number_ty *)
-
-module Params_ty: Datatype.S_with_collections with type t = number_ty list
+module Function_params_ty: Datatype.S_with_collections with type t = number_ty list
(** {3 Smart constructors} *)
@@ -98,12 +96,12 @@ val join: number_ty -> number_ty -> number_ty
(** {2 Typing} *)
(******************************************************************************)
-val type_term: use_gmp_opt:bool -> ?ctx:number_ty -> ?lenv:Params_ty.t -> term -> unit
+val type_term: use_gmp_opt:bool -> ?ctx:number_ty -> ?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: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.
If {!must_clear} is true, the typing environment is reset before translating
@@ -119,25 +117,25 @@ val clear: unit -> unit
{!type_named_predicate} has been previously computed for the given term or
predicate. *)
-val get_number_ty: term -> Params_ty.t -> number_ty
+val get_number_ty: lenv:Function_params_ty.t -> term -> number_ty
(** @return the infered type for the given term. *)
-val get_integer_op: term -> Params_ty.t -> number_ty
+val get_integer_op: lenv:Function_params_ty.t -> term -> number_ty
(** @return the infered type for the top operation of the given term.
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
-val get_integer_op_of_predicate: predicate -> Params_ty.t -> number_ty
+val get_integer_op_of_predicate: lenv:Function_params_ty.t -> predicate -> number_ty
(** @return the infered type for the top operation of the given predicate. *)
-val get_typ: term -> Params_ty.t -> typ
+val get_typ: lenv:Function_params_ty.t -> term -> typ
(** Get the type which the given term must be generated to. *)
-val get_op: term -> Params_ty.t -> typ
+val get_op: lenv:Function_params_ty.t -> term -> typ
(** Get the type which the operation on top of the given term must be generated
to. *)
-val get_cast: term -> Params_ty.t -> typ option
+val get_cast: lenv:Function_params_ty.t -> term -> typ option
(** Get the type which the given term must be converted to (if any). *)
val get_cast_of_predicate: predicate -> typ option
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 e90ceb0c7ad69771f333cd2ad4b3dc52cd8e41f8..43b11a26c740468c066a20f84d964948a20eef61 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
@@ -239,9 +239,9 @@ let to_exp ~loc kf env pot label =
| Lscope.PoT_pred _ ->
Cil.intType
| Lscope.PoT_term t ->
- begin match Typing.get_number_ty t (Env.Local_vars.get env) with
+ begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
| Typing.(C_integer _ | C_float _ | Nan) ->
- Typing.get_typ t (Env.Local_vars.get env)
+ Typing.get_typ ~lenv:(Env.Local_vars.get env) t
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
@@ -266,7 +266,7 @@ let to_exp ~loc kf env pot label =
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 t_size (Env.Local_vars.get env) with
+ 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
@@ -318,7 +318,7 @@ let to_exp ~loc kf env pot label =
variable declarations. *)
[ Smart_stmt.block_stmt block ], env
| Lscope.PoT_term t ->
- begin match Typing.get_number_ty t (Env.Local_vars.get env) with
+ begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
| Typing.(C_integer _ | C_float _ | Nan) ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 6c4ad3575708e76bc817a0cb52ae493f4f04169b..5b4947fcf7f447e7b691a50a65a2e4734463cc2f 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -167,7 +167,8 @@ end
(** Convert the given assumes clauses list to a single [predicate] *)
let assumes_predicate env assumes =
- let p = List.fold_left
+ let p =
+ List.fold_left
(fun acc p ->
let pred = p.ip_content.tp_statement in
let loc = pred.pred_loc in
@@ -176,7 +177,9 @@ let assumes_predicate env assumes =
Logic_const.unamed ~loc pred.pred_content))
Logic_const.ptrue
assumes
- in Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) p; p
+ in
+ Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) p;
+ p
let create ~loc spec =
(* Create a hashtable to associate a behavior name with an index *)
diff --git a/src/plugins/e-acsl/src/code_generator/env.ml b/src/plugins/e-acsl/src/code_generator/env.ml
index 4fcbc9bb0839021ca84e4d59ebe4ee687646163a..5e18820e027bce258162e885affe4b1cce3e882a 100644
--- a/src/plugins/e-acsl/src/code_generator/env.ml
+++ b/src/plugins/e-acsl/src/code_generator/env.ml
@@ -76,7 +76,7 @@ type t = {
(* list of loop environment for each currently visited loops *)
cpt: int;
(* counter used when generating variables *)
- local_vars: Typing.Params_ty.t list
+ local_vars: Typing.Function_params_ty.t list
(* type of variables used in calls to logic functions and predicates *)
}
@@ -385,7 +385,7 @@ end
let emitter =
Emitter.create
"E_ACSL"
- [ Emitter.Code_annot ; Emitter.Funspec ]
+ [ Emitter.Code_annot; Emitter.Funspec ]
~correctness:[ Options.Gmp_only.parameter ]
~tuning:[]
@@ -561,15 +561,6 @@ module Local_vars = struct
try List.hd env.local_vars
with Failure _ -> []
- (* let clear env =
- * Options.feedback "clearing environment '%a'" Typing.Params_ty.pretty (get env);
- * let tl =
- * try List.tl env.local_vars
- * with Failure s when String.equal s "tl" -> Options.fatal "Trying to clear an non-existing environment of local variables"
- * in
- * let env =
- * {env with local_vars = tl}
- * in Options.feedback "new local environment is '%a'" Typing.Params_ty.pretty (get env); env *)
end
let handle_error f env =
diff --git a/src/plugins/e-acsl/src/code_generator/env.mli b/src/plugins/e-acsl/src/code_generator/env.mli
index ae07d5991dd8480d9e533e32d72dfb27ac4964d2..f441c60d18dca9c0811b8ffe59306483183870b0 100644
--- a/src/plugins/e-acsl/src/code_generator/env.mli
+++ b/src/plugins/e-acsl/src/code_generator/env.mli
@@ -195,11 +195,9 @@ val emitter : Emitter.t
module Local_vars: sig
val create: t -> t
val add: t -> Typing.number_ty -> t
- val get: t -> Typing.Params_ty.t
- (* val clear: t -> t *)
+ val get: t -> Typing.Function_params_ty.t
end
-
(* ************************************************************************** *)
(** {2 Context for error handling} *)
(* ************************************************************************** *)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index acd69b7420aa93cc479ec30f7c5d075cbdf27cf8..36dc3d86838344902f8fce37aa8b875464150c54 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -864,21 +864,22 @@ let reset_all ast =
let inject () =
Gmp_types.init ();
let ast = Ast.get () in
+ let current_project = Project.current() in
Options.feedback ~level:2
"preprocessing annotations in project %a"
- Project.pretty (Project.current ());
+ Project.pretty current_project;
Preprocess_predicates.preprocess ast;
Options.feedback ~level:2
"normalizing quantifiers in project %a"
- Project.pretty (Project.current ());
+ Project.pretty current_project;
Bound_variables.preprocess ast;
Options.feedback ~level:2
"typing annotations in project %a"
- Project.pretty (Project.current ());
+ Project.pretty current_project;
Preprocess_typing.type_program ast;
Options.feedback ~level:2
"injecting annotations as code in project %a"
- Project.pretty (Project.current ());
+ Project.pretty current_project;
inject_in_file ast;
reset_all ast;
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index e051b016fdcb2782e004af5584aadf5edef6c015..374bfe5499cc3c792d04bd4b3074c1405c483c2e 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -267,7 +267,7 @@ let generate_kf ~loc fname env ret_ty params_ty li =
(* for each logic_info, associate its possible profiles, i.e. the types of its
parameters + the generated varinfo for the function *)
let memo_tbl:
- kernel_function Typing.Params_ty.Hashtbl.t Logic_info.Hashtbl.t
+ kernel_function Typing.Function_params_ty.Hashtbl.t Logic_info.Hashtbl.t
= Logic_info.Hashtbl.create 7
let reset () = Logic_info.Hashtbl.clear memo_tbl
@@ -283,10 +283,10 @@ let add_generated_functions globals =
predicate *)
let params = Logic_info.Hashtbl.find memo_tbl li in
let add_fundecl kf acc =
- GFunDecl(Cil.empty_funspec() , Kernel_function.get_vi kf, loc)
+ GFunDecl(Cil.empty_funspec (), Kernel_function.get_vi kf, loc)
:: acc
in
- aux (Typing.Params_ty.Hashtbl.fold_sorted (fun _ -> add_fundecl) params acc) l
+ aux (Typing.Function_params_ty.Hashtbl.fold_sorted (fun _ -> add_fundecl) params acc) l
with Not_found ->
aux acc l)
| g :: l ->
@@ -303,7 +303,7 @@ let add_generated_functions globals =
in
let rev_globals =
Logic_info.Hashtbl.fold_sorted
- (fun _ -> Typing.Params_ty.Hashtbl.fold_sorted (fun _ -> add_fundec))
+ (fun _ -> Typing.Function_params_ty.Hashtbl.fold_sorted (fun _ -> add_fundec))
memo_tbl
rev_globals
in
@@ -312,10 +312,10 @@ let add_generated_functions globals =
(* Generate (and memoize) the function body and create the call to the
generated function. *)
let function_to_exp ~loc fname env kf t li params_ty args =
- let ret_ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ret_ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let gen tbl =
let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
- Typing.Params_ty.Hashtbl.add tbl params_ty kf;
+ Typing.Function_params_ty.Hashtbl.add tbl params_ty kf;
vi, gen_body
in
(* memoise the function's varinfo *)
@@ -323,12 +323,12 @@ let function_to_exp ~loc fname env kf t li params_ty args =
try
let h = Logic_info.Hashtbl.find memo_tbl li in
try
- let kf = Typing.Params_ty.Hashtbl.find h params_ty in
+ let kf = Typing.Function_params_ty.Hashtbl.find h params_ty in
Kernel_function.get_vi kf,
(fun () -> ()) (* body generation already planified *)
with Not_found -> gen h
with Not_found ->
- let h = Typing.Params_ty.Hashtbl.create 7 in
+ let h = Typing.Function_params_ty.Hashtbl.create 7 in
Logic_info.Hashtbl.add memo_tbl li h;
gen h
in
@@ -392,7 +392,7 @@ let tapp_to_exp ~adata kf env ?eargs tapp =
let _, e, adata, env =
if Builtins.mem li.l_var_info.lv_name then
match l with
- | _::_ -> Error.not_yet "e-acsl builtin functions with labels"
+ | _::_ -> Error.not_yet "E-ACSL built-in functions with labels"
| [] ->
(* E-ACSL built-in function call *)
let args, adata, env =
@@ -446,40 +446,37 @@ let tapp_to_exp ~adata kf env ?eargs tapp =
"[Tapp] unexpected number of arguments when calling %s"
fname;
eargs, adata, env
+ in
+ try
+ List.fold_right2
+ (fun targ earg (params_ty, args, env) ->
+ let param_ty = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) targ in
+ let e, env =
+ try
+ let ty = Typing.typ_of_number_ty param_ty in
+ Typed_number.add_cast
+ ~loc
+ env
+ kf
+ (Some ty)
+ Typed_number.C_number
+ (Some targ)
+ earg
+ with Typing.Not_a_number ->
+ earg, env
+ in
+ param_ty :: params_ty, e :: args, env)
+ targs eargs
+ ([], [], env)
+ with Invalid_argument _ ->
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname
in
- try
- List.fold_right2
- (fun targ earg (params_ty, args, adata, env) ->
- let param_ty = Typing.get_number_ty targ (Env.Local_vars.get env) in
- let e, env =
- try
- let ty = Typing.typ_of_number_ty param_ty in
- Typed_number.add_cast
- ~loc
- env
- kf
- (Some ty)
- Typed_number.C_number
- (Some targ)
- earg
- with Typing.Not_a_number ->
- earg, env
- in
- param_ty :: params_ty, e :: args, adata, env)
- targs eargs
- ([], [], adata, env)
- with Invalid_argument _ ->
- Options.fatal
- "[Tapp] unexpected number of arguments when calling %s"
- fname
- in
- let gen_fname =
- Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
- in
- let vi, e, env =
- function_to_exp ~loc gen_fname env kf tapp li params_ty args
- in
- vi, e, adata, env
+ let gen_fname =
+ Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
+ in
+ function_to_exp ~loc gen_fname env kf tapp li params_ty args;
in
e, adata, env
| _ ->
diff --git a/src/plugins/e-acsl/src/code_generator/loops.ml b/src/plugins/e-acsl/src/code_generator/loops.ml
index f4554a4259cee20eaccad9c91cc944e9bb317487..54a07a2bb591a48cfcc3dce51158b2e511242c1e 100644
--- a/src/plugins/e-acsl/src/code_generator/loops.ml
+++ b/src/plugins/e-acsl/src/code_generator/loops.ml
@@ -66,7 +66,7 @@ let handle_annotations env kf stmt =
let env = Env.set_annotation_kind env Smart_stmt.Variant in
let env = Env.push env in
Typing.type_term ~use_gmp_opt:true t;
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
if Gmp_types.is_t ty then Error.not_yet "loop variant using GMP";
let e, _, env = !term_to_exp_ref ~adata:Assert.no_data kf env t in
let vi_old, e_old, env =
@@ -289,8 +289,8 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Typing.type_term ~use_gmp_opt:false t1;
Typing.type_term ~use_gmp_opt:false t2;
let ctx =
- let ty1 = Typing.get_number_ty t1 (Env.Local_vars.get env) in
- let ty2 = Typing.get_number_ty t2 (Env.Local_vars.get env) in
+ let ty1 = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t1 in
+ let ty2 = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t2 in
Typing.join ty1 ty2
in
let t_plus_one ?ty t =
@@ -380,8 +380,9 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
let adata, env = Assert.empty ~loc kf env in
let e, adata, env =
(* Even though p is considered a RTE, it was generated while
- typing the loop was already typed at this moment *)
- !predicate_to_exp_ref ~adata kf (Env.push env) p
+ typing the loop, and was already typed at this moment. Thus
+ there is no need to type it again *)
+ !predicate_to_exp_ref kf (Env.push env) p
in
let stmt, env =
Assert.runtime_check
@@ -411,7 +412,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
Env.Logic_binding.remove env logic_x;
[ start ; stmt ], env
| Lscope.Lvs_let(lv, t) :: lscope_vars' ->
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
let e, _, env = term_to_exp kf env t in
let ty = Cil.typeOf e in
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 00ba77de3992fa337b41f423c54e47f28da5392c..efa66fcbe4e99641199a0b41ebc7af42151f979b 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -262,7 +262,7 @@ let range_to_ptr_and_size ~adata ~loc kf env ptr r p =
in
Typing.type_term ~use_gmp_opt:false size_term;
let size, adata, env =
- match Typing.get_number_ty size_term (Env.Local_vars.get env) with
+ match Typing.get_number_ty size_term ~lenv:(Env.Local_vars.get env) with
| Typing.Gmpz ->
(* Start by translating [size_term] to an expression so that the full term
with [\let] is not passed around. *)
@@ -331,7 +331,6 @@ let fname_to_pred ?loc name args =
| _ ->
Options.fatal "Unsupported function '%s'" name
-
(* [extract_quantifiers ~loc args] iterates over each argument in [args] and if
that argument contains a non-explicit range, tries to extract a universal
quantifier representing the range and returns an updated argument for this
diff --git a/src/plugins/e-acsl/src/code_generator/smart_term.ml b/src/plugins/e-acsl/src/code_generator/smart_term.ml
index 2290a3a203e6d0538d1621a14e2e6311a89d489c..73746edfebf37ebcb7b279349fb32b81267d9c60 100644
--- a/src/plugins/e-acsl/src/code_generator/smart_term.ml
+++ b/src/plugins/e-acsl/src/code_generator/smart_term.ml
@@ -37,7 +37,6 @@ let is_pointer_type cty =
| TPtr(_,_)
| TArray(_,_,_,_) -> true
-
let deref_cty cty =
let cty = Cil.unrollType cty in
match cty with
@@ -51,9 +50,9 @@ let deref_cty cty =
| TEnum (_,_)
-> Options.fatal "recieved the type %a when a pointer type was expected"
Printer.pp_typ cty
- | TPtr(cty,_) -> cty
- | TArray(cty,_,_,_) -> cty
-
+ | TPtr(cty,_)
+ | TArray(cty,_,_,_)
+ -> cty
let deref_lty ?cty lty = match lty with
| Lreal | Lvar _ | Larrow (_ , _) | Ltype (_ , _)->
@@ -66,14 +65,13 @@ let deref_lty ?cty lty = match lty with
Printer.pp_logic_type lty
| Some cty -> Ctype (deref_cty cty)
-
let logic_type ?cty = function
| TVar vi -> vi.lv_type
| TResult ty -> Ctype ty
| TMem tm -> deref_lty ?cty tm.term_type
-let lval ?cty ~loc tlv =
- Logic_const.term ~loc (TLval tlv) (logic_type ?cty (fst tlv))
+let lval ?cty ~loc (thost,_ as tlv) =
+ Logic_const.term ~loc (TLval tlv) (logic_type ?cty thost)
let deref ?cty ~loc tlv = lval ?cty ~loc (TMem tlv, TNoOffset)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index cce162614b7b319595c70d66ce0560a7d707c3ca..3297bd317cc68da2501063ad0a46e47876410df6 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -39,14 +39,14 @@ let relation_to_binop = function
| Req -> Eq
| Rneq -> Ne
-let constant_to_exp ~loc t c env =
+let constant_to_exp ~loc env t c =
let mk_real s =
let s = Rational.normalize_str s in
Cil.mkString ~loc s, Typed_number.Str_R
in
match c with
| Integer(n, _repr) ->
- let ity = Typing.get_number_ty t (Env.Local_vars.get env) in
+ let ity = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
(match ity with
| Typing.Nan -> assert false
| Typing.Real -> Error.not_yet "real number constant"
@@ -57,7 +57,7 @@ let constant_to_exp ~loc t c env =
| Typing.C_float fkind ->
Cil.kfloat ~loc fkind (Int64.to_float (Integer.to_int64 n)), C_number
| Typing.C_integer kind ->
- let cast = Typing.get_cast t (Env.Local_vars.get env) in
+ let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
match cast, kind with
| Some ty, (ILongLong | IULongLong) when Gmp_types.Z.is_t ty ->
(* too large integer *)
@@ -91,7 +91,7 @@ let conditional_to_exp ?(name="if") loc kf t_opt e1 (e2, env2) (e3, env3) =
| _ ->
let ty = match t_opt with
| None (* predicate *) -> Cil.intType
- | Some t -> Typing.get_typ t (Env.Local_vars.get env)
+ | Some t -> Typing.get_typ ~lenv:(Env.Local_vars.get env) t
in
let _, e, env =
Env.new_var
@@ -198,8 +198,8 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
let e, adata, env =
match name.lv_name,lambda.term_node with
| "\\sum", Tlambda([ k ] ,lt) ->
- let ty_sum = Typing.get_typ t (Env.Local_vars.get env) in
- let ty_k = match Typing.get_cast t_min (Env.Local_vars.get env) with
+ let ty_sum = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+ let ty_k = match Typing.get_cast ~lenv:(Env.Local_vars.get env) t_min with
|Some e ->e
| _ -> Options.fatal "unexpected error in \\sum translation"
in
@@ -299,7 +299,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let loc = t.term_loc in
match t.term_node with
| TConst c ->
- let c, strnum = constant_to_exp ~loc t c env in
+ let c, strnum = constant_to_exp ~loc env t c in
c, adata, env, strnum, ""
| TLval lv ->
let lv, env, name = tlval_to_lval kf env lv in
@@ -329,7 +329,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let adata, env = Assert.register_term ~loc kf env t e adata in
e, adata, env, Typed_number.C_number, "alignof"
| TUnOp(Neg | BNot as op, t') ->
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let e, adata, env = term_to_exp ~adata kf env t' in
if Gmp_types.Z.is_t ty then
let name, vname = match op with
@@ -352,12 +352,12 @@ and context_insensitive_term_to_exp ~adata kf env t =
else
Cil.new_exp ~loc (UnOp(op, e, ty)), adata, env, Typed_number.C_number, ""
| TUnOp(LNot, t) ->
- let ty = Typing.get_op t (Env.Local_vars.get env) in
+ let ty = Typing.get_op ~lenv:(Env.Local_vars.get env) t in
if Gmp_types.Z.is_t ty then
(* [!t] is converted into [t == 0] *)
let zero = Logic_const.tinteger 0 in
- let ctx = Typing.get_number_ty t (Env.Local_vars.get env) in
- Typing.type_term ~use_gmp_opt:true ~ctx (Env.Local_vars.get env) zero;
+ let ctx = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
+ Typing.type_term ~use_gmp_opt:true ~ctx ~lenv:(Env.Local_vars.get env) zero;
let e, adata, env =
comparison_to_exp
~adata
@@ -379,9 +379,15 @@ and context_insensitive_term_to_exp ~adata kf env t =
e, adata, env, Typed_number.C_number, ""
end
| TBinOp(PlusA | MinusA | Mult as bop, t1, t2) ->
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+<<<<<<< variant A
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let e1, adata, env = term_to_exp ~adata kf env t1 in
let e2, adata, env = term_to_exp ~adata kf env t2 in
+>>>>>>> variant B
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
+ let e1, env = term_to_exp kf env t1 in
+ let e2, env = term_to_exp kf env t2 in
+======= end
if Gmp_types.Z.is_t ty then
let name = Gmp.name_of_mpz_arith_bop bop in
let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
@@ -402,7 +408,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
e, adata, env, Typed_number.C_number, ""
end
| TBinOp(Div | Mod as bop, t1, t2) ->
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let e1, adata, env = term_to_exp ~adata kf env t1 in
(* Creating a second assertion context that will hold the data contributing
to the guard of the denominator. The context will be merged to [adata]
@@ -413,7 +419,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
if Gmp_types.Z.is_t ty then
(* TODO: preventing division by zero should not be required anymore.
RTE should do this automatically. *)
- let ctx = Typing.get_number_ty t (Env.Local_vars.get env) in
+ let ctx = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
let t = Some t in
let name = Gmp.name_of_mpz_arith_bop bop in
(* [TODO] can now do better since the type system got some info about
@@ -458,14 +464,14 @@ and context_insensitive_term_to_exp ~adata kf env t =
end
| TBinOp(Lt | Gt | Le | Ge | Eq | Ne as bop, t1, t2) ->
(* comparison operators *)
- let ity = Typing.get_integer_op t (Env.Local_vars.get env) in
+ let ity = Typing.get_integer_op ~lenv:(Env.Local_vars.get env) t in
let e, adata, env =
comparison_to_exp ~adata ~loc kf env ity bop t1 t2 (Some t)
in
e, adata, env, Typed_number.C_number, ""
| TBinOp((Shiftlt | Shiftrt) as bop, t1, t2) ->
(* left/right shift *)
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
(* Creating secondary assertion contexts [adata1] and [adata2] to hold the
data contributing to the guards of [t1] and [t2].
Both secondary contexts will be merged to [adata] afterward so that the
@@ -488,7 +494,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
| TLogic_coerce (_, t) -> term_to_name t
| _ -> ""
in
- let ctx = Typing.get_number_ty t (Env.Local_vars.get env) in
+ let ctx = Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t in
let bop_name = Misc.name_of_binop bop in
let e1_name = term_to_name t1 in
let e2_name = term_to_name t2 in
@@ -670,7 +676,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
e, adata, env, Typed_number.C_number, ""
| TBinOp((BOr | BXor | BAnd) as bop, t1, t2) ->
(* other logic/arith operators *)
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let e1, adata, env = term_to_exp ~adata kf env t1 in
let e2, adata, env = term_to_exp ~adata kf env t2 in
if Gmp_types.Z.is_t ty then
@@ -705,11 +711,11 @@ and context_insensitive_term_to_exp ~adata kf env t =
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
| TBinOp(MinusPP, t1, t2) ->
- begin match Typing.get_number_ty t (Env.Local_vars.get env) with
+ begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
| Typing.C_integer _ ->
let e1, adata, env = term_to_exp ~adata kf env t1 in
let e2, adata, env = term_to_exp ~adata kf env t2 in
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let e = Cil.new_exp ~loc (BinOp(MinusPP, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
| Typing.Gmpz ->
@@ -848,7 +854,7 @@ and term_to_exp ~adata kf env t =
let generate_rte = Env.generate_rte env in
Options.feedback ~dkey ~level:4 "translating term %a (rte? %b)in local \
environment '%a'"
- Printer.pp_term t generate_rte Typing.Params_ty.pretty
+ Printer.pp_term t generate_rte Typing.Functions_params_ty.pretty
(Env.Local_vars.get env);
Extlib.flatten
(Env.with_rte_and_result env false
@@ -857,7 +863,7 @@ and term_to_exp ~adata kf env t =
context_insensitive_term_to_exp ~adata kf env t
in
let env = if generate_rte then translate_rte kf env e else env in
- let cast = Typing.get_cast t (Env.Local_vars.get env) in
+ let cast = Typing.get_cast ~lenv:(Env.Local_vars.get env) t in
let name = if name = "" then None else Some name in
Extlib.nest
adata
@@ -991,10 +997,10 @@ and at_to_exp_no_lscope env kf t_opt label e =
and env_of_li ~adata li kf env loc =
let t = Misc.term_of_li li in
- let ty = Typing.get_typ t (Env.Local_vars.get env) in
+ let ty = Typing.get_typ ~lenv:(Env.Local_vars.get env) t in
let vi, vi_e, env = Env.Logic_binding.add ~ty env kf li.l_var_info in
let e, adata, env = term_to_exp ~adata kf env t in
- let stmt = match Typing.get_number_ty t (Env.Local_vars.get env) with
+ let stmt = match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
| Typing.(C_integer _ | C_float _ | Nan) ->
Smart_stmt.assigns ~loc ~result:(Cil.var vi) e
| Typing.Gmpz ->
@@ -1016,24 +1022,11 @@ and predicate_content_to_exp ~adata ?name kf env p =
| Pfalse -> Cil.zero ~loc, env
| Ptrue -> Cil.one ~loc, env
| Papp _ -> Options.fatal "Reached applied predicate: %a" Printer.pp_predicate p;
- (* (\* Simply use the implementation of Tapp(li, labels, args).
- * To achieve this, we create a clone of [li] for which the type is
- * transformed from [None] (type of predicates) to
- * [Some int] (type as a term). *\)
- * let prj = Project.current () in
- * let o = object inherit Visitor.frama_c_copy prj end in
- * let li = Visitor.visitFramacLogicInfo o li in
- * let lty = Ctype Cil.intType in
- * li.l_type <- Some lty;
- * let tapp = Logic_const.term ~loc (Tapp(li, labels, args)) lty in
- * (\* Typing.type_term ~use_gmp_opt:false ~ctx:Typing.c_int tapp; *\)
- * let e, env = term_to_exp kf env tapp in
- * e, env *)
| Pdangling _ -> Env.not_yet env "\\dangling"
| Pobject_pointer _ -> Env.not_yet env "\\object_pointer"
| Pvalid_function _ -> Env.not_yet env "\\valid_function"
| Prel(rel, t1, t2) ->
- let ity = Typing.get_integer_op_of_predicate p (Env.Local_vars.get env) in
+ let ity = Typing.get_integer_op_of_predicate ~lenv:(Env.Local_vars.get env) p in
comparison_to_exp ~adata ~loc kf env ity (relation_to_binop rel) t1 t2 None
| Pand(p1, p2) ->
(* p1 && p2 <==> if p1 then p2 else false *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate_annots.ml b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
index a66bab6dc5ad918547dd677269b4620fc61ec37e..a99ab2ee5f0b51cbc84bfc0cd91ec2396c56aaf5 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_annots.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_annots.ml
@@ -53,7 +53,6 @@ let () =
Preprocess_typing.must_translate_ref := must_translate;
Preprocess_typing.must_translate_opt_ref := must_translate_opt
-
let pre_funspec kf kinstr env funspec =
let unsupported f x = ignore (Env.handle_error (fun env -> f x; env) env) in
let convert_unsupported_clauses env =
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 480c215eb67faba9f01b9171ef5697184a1bc699..bfde94f602c323ae8f4aab177bfc801168185c3d 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -26,7 +26,6 @@ exception Ignored
exception Typing_error of string
exception Not_yet of string
-
val untypable: string -> 'a
(** Type error built from the given argument. *)
diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index 2099b66b8aae4b364ac1f040b811db626654a1e8..c50124bb9de035fc031e4bbab33608bcb1df5640 100644
--- a/src/plugins/e-acsl/tests/arith/functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/functions_rec.c
@@ -21,11 +21,9 @@
n < 0x7fffffffffffffffL ? 0x7fffffffffffffffL :
6; */
-
/*@ logic integer f5(integer n) =
n >= 0 ? 0 : f5(n + 1) + n; */
-
int main (void) {
/*@ assert f1(0) == 0; */ ;
/*@ assert f1(1) == 1; */ ;
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
index f35574580de4f164c9060907320c0ff9bff9081b..91cd6ea7f269c35e3511a186c0619dff6252e6c0 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
@@ -1,12 +1,12 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/arith/functions_rec.c:30: Warning:
+[eva:alarm] tests/arith/functions_rec.c:28: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:30: Warning:
+[eva:alarm] tests/arith/functions_rec.c:28: Warning:
assertion got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:31: Warning:
+[eva:alarm] tests/arith/functions_rec.c:29: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:31: Warning:
+[eva:alarm] tests/arith/functions_rec.c:29: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:10: Warning:
accessing uninitialized left-value.
@@ -30,9 +30,9 @@
effects will be ignored
[eva:locals-escaping] tests/arith/functions_rec.c:10: Warning:
locals {__gen_e_acsl__4, __gen_e_acsl_le, __gen_e_acsl_if} escaping the scope of __gen_e_acsl_f1_3 through __gen_e_acsl_f1_5
-[eva:alarm] tests/arith/functions_rec.c:32: Warning:
+[eva:alarm] tests/arith/functions_rec.c:30: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:32: Warning:
+[eva:alarm] tests/arith/functions_rec.c:30: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:13: Warning:
accessing uninitialized left-value.
@@ -199,17 +199,17 @@
2147483647;
[eva:locals-escaping] tests/arith/functions_rec.c:13: Warning:
locals {__gen_e_acsl_f2_15, __gen_e_acsl_f2_17, __gen_e_acsl_f2_19} escaping the scope of a block of __gen_e_acsl_f2 through __gen_e_acsl_if_6
-[eva:alarm] tests/arith/functions_rec.c:34: Warning:
+[eva:alarm] tests/arith/functions_rec.c:32: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&__gen_e_acsl_if_6);
-[eva:locals-escaping] tests/arith/functions_rec.c:34: Warning:
+[eva:locals-escaping] tests/arith/functions_rec.c:32: Warning:
locals {__gen_e_acsl_if_6} escaping the scope of __gen_e_acsl_f2 through \result<__gen_e_acsl_f2>
-[eva:alarm] tests/arith/functions_rec.c:34: Warning:
+[eva:alarm] tests/arith/functions_rec.c:32: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&__gen_e_acsl_f2_20);
-[eva:alarm] tests/arith/functions_rec.c:34: Warning:
+[eva:alarm] tests/arith/functions_rec.c:32: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:34: Warning:
+[eva:alarm] tests/arith/functions_rec.c:32: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:17: Warning:
accessing uninitialized left-value.
@@ -289,17 +289,17 @@
assert (int)(__gen_e_acsl_g_2 * __gen_e_acsl_f3_7) - 5 ≤ 2147483647;
[eva:locals-escaping] tests/arith/functions_rec.c:17: Warning:
locals {__gen_e_acsl_g_2, __gen_e_acsl_f3_7} escaping the scope of a block of __gen_e_acsl_f3 through __gen_e_acsl_if_9
-[eva:alarm] tests/arith/functions_rec.c:36: Warning:
+[eva:alarm] tests/arith/functions_rec.c:34: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&__gen_e_acsl_if_9);
-[eva:locals-escaping] tests/arith/functions_rec.c:36: Warning:
+[eva:locals-escaping] tests/arith/functions_rec.c:34: Warning:
locals {__gen_e_acsl_if_9} escaping the scope of __gen_e_acsl_f3 through \result<__gen_e_acsl_f3>
-[eva:alarm] tests/arith/functions_rec.c:36: Warning:
+[eva:alarm] tests/arith/functions_rec.c:34: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&__gen_e_acsl_f3_8);
-[eva:alarm] tests/arith/functions_rec.c:36: Warning:
+[eva:alarm] tests/arith/functions_rec.c:34: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:36: Warning:
+[eva:alarm] tests/arith/functions_rec.c:34: Warning:
assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:20: Warning:
accessing uninitialized left-value.
@@ -345,14 +345,18 @@
assert ¬\dangling(&__gen_e_acsl_f4_7);
[eva:locals-escaping] :0: Warning:
locals {__gen_e_acsl_f4_7} escaping the scope of a block of __gen_e_acsl_f4 through __gen_e_acsl_if_15
-[eva:alarm] tests/arith/functions_rec.c:38: Warning:
+[eva:alarm] tests/arith/functions_rec.c:36: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&__gen_e_acsl_if_15);
-[eva:locals-escaping] tests/arith/functions_rec.c:38: Warning:
+[eva:locals-escaping] tests/arith/functions_rec.c:36: Warning:
locals {__gen_e_acsl_if_15} escaping the scope of __gen_e_acsl_f4 through \result<__gen_e_acsl_f4>
-[eva:alarm] tests/arith/functions_rec.c:38: Warning:
+[eva:alarm] tests/arith/functions_rec.c:36: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&__gen_e_acsl_f4_8);
+[eva:alarm] tests/arith/functions_rec.c:36: Warning:
+ function __e_acsl_assert, behavior blocking: precondition got status unknown.
+[eva:alarm] tests/arith/functions_rec.c:36: Warning:
+ assertion got status unknown.
[eva:alarm] tests/arith/functions_rec.c:38: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:38: Warning:
@@ -361,7 +365,3 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] tests/arith/functions_rec.c:40: Warning:
assertion got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:42: Warning:
- function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[eva:alarm] tests/arith/functions_rec.c:42: Warning:
- assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
index 761ac51f9842286a3cc03fb67ce6bfeb36d7b9c1..9461cbf897dd683fc48fb1a354524f862b68343b 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
+++ b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
@@ -71,7 +71,7 @@ int main(void)
__gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_8),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__7));
__e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","main","f1(0) == 0",
- "tests/arith/functions_rec.c",30);
+ "tests/arith/functions_rec.c",28);
__gmpz_clear(__gen_e_acsl_f1_8);
__gmpz_clear(__gen_e_acsl__7);
}
@@ -85,7 +85,7 @@ int main(void)
__gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_10),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__8));
__e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","main","f1(1) == 1",
- "tests/arith/functions_rec.c",31);
+ "tests/arith/functions_rec.c",29);
__gmpz_clear(__gen_e_acsl_f1_10);
__gmpz_clear(__gen_e_acsl__8);
}
@@ -99,7 +99,7 @@ int main(void)
__gen_e_acsl_eq_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f1_12),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__9));
__e_acsl_assert(__gen_e_acsl_eq_3 == 0,1,"Assertion","main",
- "f1(100) == 5050","tests/arith/functions_rec.c",32);
+ "f1(100) == 5050","tests/arith/functions_rec.c",30);
__gmpz_clear(__gen_e_acsl_f1_12);
__gmpz_clear(__gen_e_acsl__9);
}
@@ -109,7 +109,7 @@ int main(void)
__gen_e_acsl_f2_20 = __gen_e_acsl_f2(7);
/*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f2_20); */
__e_acsl_assert(__gen_e_acsl_f2_20 == 1,1,"Assertion","main",
- "f2(7) == 1","tests/arith/functions_rec.c",34);
+ "f2(7) == 1","tests/arith/functions_rec.c",32);
}
/*@ assert f2(7) ≡ 1; */ ;
{
@@ -117,7 +117,7 @@ int main(void)
__gen_e_acsl_f3_8 = __gen_e_acsl_f3(6);
/*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f3_8); */
__e_acsl_assert(__gen_e_acsl_f3_8 == -5,1,"Assertion","main",
- "f3(6) == -5","tests/arith/functions_rec.c",36);
+ "f3(6) == -5","tests/arith/functions_rec.c",34);
}
/*@ assert f3(6) ≡ -5; */ ;
{
@@ -125,7 +125,7 @@ int main(void)
__gen_e_acsl_f4_8 = __gen_e_acsl_f4(9);
/*@ assert Eva: dangling_pointer: ¬\dangling(&__gen_e_acsl_f4_8); */
__e_acsl_assert(__gen_e_acsl_f4_8 > 0UL,1,"Assertion","main","f4(9) > 0",
- "tests/arith/functions_rec.c",38);
+ "tests/arith/functions_rec.c",36);
}
/*@ assert f4(9) > 0; */ ;
{
@@ -137,7 +137,7 @@ int main(void)
__gen_e_acsl_eq_4 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_f5_8),
(__e_acsl_mpz_struct const *)(__gen_e_acsl__32));
__e_acsl_assert(__gen_e_acsl_eq_4 == 0,1,"Assertion","main","f5(0) == 0",
- "tests/arith/functions_rec.c",40);
+ "tests/arith/functions_rec.c",38);
__gmpz_clear(__gen_e_acsl_f5_8);
__gmpz_clear(__gen_e_acsl__32);
}
@@ -154,7 +154,7 @@ int main(void)
(__e_acsl_mpz_struct const *)(__gen_e_acsl__33));
__e_acsl_assert(__gen_e_acsl_eq_5 == 0,1,"Assertion","main",
"\\let n = 0 == 0? 0x7fffffffffffffffL: -1; f5(n) == 0",
- "tests/arith/functions_rec.c",42);
+ "tests/arith/functions_rec.c",40);
__gmpz_clear(__gen_e_acsl_f5_10);
__gmpz_clear(__gen_e_acsl__33);
}