diff --git a/src/plugins/e-acsl/src/analyses/bound_variables.ml b/src/plugins/e-acsl/src/analyses/bound_variables.ml
index 447a396a39957c009b90080dca5222f5c92117a4..4cc317c1f9c028d086deecb18b1f059928bef270 100644
--- a/src/plugins/e-acsl/src/analyses/bound_variables.ml
+++ b/src/plugins/e-acsl/src/analyses/bound_variables.ml
@@ -698,18 +698,18 @@ end
match a with
| Dfun_or_pred (li,loc) ->
(match li.l_body with
- | LBpred p ->
- (match Logic_normalizer.get_pred p with
+ | LBpred p ->
+ (match Logic_normalizer.get_pred p with
| PoT_pred p -> process_quantif ~loc p
| PoT_term _ -> ())
- | _ -> ())
+ | _ -> ())
| _ -> ()
- let do_predicates () =
- Annotations.iter_global (fun _ a -> gannot a)
+ let do_predicates () =
+ Annotations.iter_global (fun _ a -> gannot a)
- let preprocessor = object
+ let preprocessor = object
inherit E_acsl_visitor.visitor
method !vpredicate p =
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 fe81e164e286babf865fd97aca574a98d6f576e2..13576ff7969ea81738d8f58192e09ab0d57b7704 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -407,105 +407,105 @@ let raise_errors = function
let app_to_exp ~adata ~loc ?tapp kf env ?eargs
((li, targs) : logic_info * term list) =
- let fname = li.l_var_info.lv_name in
- (* build the varinfo (as an expression) which stores the result of the
- function call. *)
- let _, e, adata, env =
- if Builtins.mem li.l_var_info.lv_name then
- (* E-ACSL built-in function call *)
- let args, adata, env =
- match eargs with
- | None ->
- List.fold_right
- (fun targ (l, adata, env) ->
- let e, adata, env = !term_to_exp_ref ~adata kf env targ in
- e :: l, adata, env)
- targs
- ([], adata, env)
- | Some eargs ->
- if List.compare_lengths targs eargs != 0 then
- Options.fatal
- "[Tapp] unexpected number of arguments when calling %s"
- fname;
- eargs, adata, env
+ let fname = li.l_var_info.lv_name in
+ (* build the varinfo (as an expression) which stores the result of the
+ function call. *)
+ let _, e, adata, env =
+ if Builtins.mem li.l_var_info.lv_name then
+ (* E-ACSL built-in function call *)
+ let args, adata, env =
+ match eargs with
+ | None ->
+ List.fold_right
+ (fun targ (l, adata, env) ->
+ let e, adata, env = !term_to_exp_ref ~adata kf env targ in
+ e :: l, adata, env)
+ targs
+ ([], adata, env)
+ | Some eargs ->
+ if List.compare_lengths targs eargs != 0 then
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname;
+ eargs, adata, env
+ in
+ let vi, e, env =
+ Env.new_var
+ ~loc
+ ~name:(fname ^ "_app")
+ env
+ kf
+ tapp
+ (Misc.cty (Option.get li.l_type))
+ (fun vi _ ->
+ [ Smart_stmt.rtl_call ~loc
+ ~result:(Cil.var vi)
+ ~prefix:""
+ fname
+ args ])
+ in
+ vi, e, adata, env
+ else
+ begin
+ raise_errors li.l_body;
+ (* build the arguments and compute the integer_ty of the parameters *)
+ let params_ty, args, adata, env =
+ let eargs, adata, env =
+ match eargs with
+ | None ->
+ List.fold_right
+ (fun targ (eargs, adata, env) ->
+ let e, adata, env = !term_to_exp_ref ~adata kf env targ in
+ e :: eargs, adata, env)
+ targs
+ ([], adata, env)
+ | Some eargs ->
+ if List.compare_lengths targs eargs != 0 then
+ Options.fatal
+ "[Tapp] unexpected number of arguments when calling %s"
+ fname;
+ eargs, adata, env
+ in
+ try
+ List.fold_right2
+ (fun targ earg (params_ty, args, adata, 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, 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 =
- Env.new_var
- ~loc
- ~name:(fname ^ "_app")
- env
- kf
- tapp
- (Misc.cty (Option.get li.l_type))
- (fun vi _ ->
- [ Smart_stmt.rtl_call ~loc
- ~result:(Cil.var vi)
- ~prefix:""
- fname
- args ])
+ function_to_exp ~loc ?tapp gen_fname env kf li params_ty args
in
vi, e, adata, env
- else
- begin
- raise_errors li.l_body;
- (* build the arguments and compute the integer_ty of the parameters *)
- let params_ty, args, adata, env =
- let eargs, adata, env =
- match eargs with
- | None ->
- List.fold_right
- (fun targ (eargs, adata, env) ->
- let e, adata, env = !term_to_exp_ref ~adata kf env targ in
- e :: eargs, adata, env)
- targs
- ([], adata, env)
- | Some eargs ->
- if List.compare_lengths targs eargs != 0 then
- Options.fatal
- "[Tapp] unexpected number of arguments when calling %s"
- fname;
- eargs, adata, env
- in
- try
- List.fold_right2
- (fun targ earg (params_ty, args, adata, 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, 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 ?tapp gen_fname env kf li params_ty args
- in
- vi, e, adata, env
- end
- in
- e, adata, env
+ end
+ in
+ e, adata, env
(* let tapp_to_exp ~adata kf env ?eargs tapp = *)
(* match tapp.term_node with *)