Skip to content
Snippets Groups Projects
Unverified Commit 0815414e authored by Thibaut Benjamin's avatar Thibaut Benjamin
Browse files

[e-acsl] lint

parent 92654857
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/e-acsl/src/analyses/bound_variables.ml
+ 6
− 6
View file @ 0815414e
...@@ -698,18 +698,18 @@ end ...@@ -698,18 +698,18 @@ end
match a with match a with
| Dfun_or_pred (li,loc) -> | Dfun_or_pred (li,loc) ->
(match li.l_body with (match li.l_body with
| LBpred p -> | LBpred p ->
(match Logic_normalizer.get_pred p with (match Logic_normalizer.get_pred p with
| PoT_pred p -> process_quantif ~loc p | PoT_pred p -> process_quantif ~loc p
| PoT_term _ -> ()) | PoT_term _ -> ())
| _ -> ()) | _ -> ())
| _ -> () | _ -> ()
let do_predicates () = let do_predicates () =
Annotations.iter_global (fun _ a -> gannot a) Annotations.iter_global (fun _ a -> gannot a)
let preprocessor = object let preprocessor = object
inherit E_acsl_visitor.visitor inherit E_acsl_visitor.visitor
method !vpredicate p = method !vpredicate p =
......
src/plugins/e-acsl/src/code_generator/logic_functions.ml
+ 95
− 95
View file @ 0815414e
...@@ -407,105 +407,105 @@ let raise_errors = function ...@@ -407,105 +407,105 @@ let raise_errors = function
let app_to_exp ~adata ~loc ?tapp kf env ?eargs let app_to_exp ~adata ~loc ?tapp kf env ?eargs
((li, targs) : logic_info * term list) = ((li, targs) : logic_info * term list) =
let fname = li.l_var_info.lv_name in let fname = li.l_var_info.lv_name in
(* build the varinfo (as an expression) which stores the result of the (* build the varinfo (as an expression) which stores the result of the
function call. *) function call. *)
let _, e, adata, env = let _, e, adata, env =
if Builtins.mem li.l_var_info.lv_name then if Builtins.mem li.l_var_info.lv_name then
(* E-ACSL built-in function call *) (* E-ACSL built-in function call *)
let args, adata, env = let args, adata, env =
match eargs with match eargs with
| None -> | None ->
List.fold_right List.fold_right
(fun targ (l, adata, env) -> (fun targ (l, adata, env) ->
let e, adata, env = !term_to_exp_ref ~adata kf env targ in let e, adata, env = !term_to_exp_ref ~adata kf env targ in
e :: l, adata, env) e :: l, adata, env)
targs targs
([], adata, env) ([], adata, env)
| Some eargs -> | Some eargs ->
if List.compare_lengths targs eargs != 0 then if List.compare_lengths targs eargs != 0 then
Options.fatal Options.fatal
"[Tapp] unexpected number of arguments when calling %s" "[Tapp] unexpected number of arguments when calling %s"
fname; fname;
eargs, adata, env 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 in
let vi, e, env = let vi, e, env =
Env.new_var function_to_exp ~loc ?tapp gen_fname env kf li params_ty args
~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 in
vi, e, adata, env vi, e, adata, env
else end
begin in
raise_errors li.l_body; e, adata, env
(* 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
(* let tapp_to_exp ~adata kf env ?eargs tapp = *) (* let tapp_to_exp ~adata kf env ?eargs tapp = *)
(* match tapp.term_node with *) (* match tapp.term_node with *)
......
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