Commit 7a577a16 authored by Sylvain's avatar Sylvain

Activate "unused" warning even with no contracts/body

parent d815b91d
......@@ -1217,67 +1217,61 @@ let check_used_pv e pv =
No warnings are returned if there are no body, no pre, and no (x)post.
*)
let check_unused_vars_fun (bl: Ity.pvsymbol list) (dsp: dspec_final) eff_reads =
(* TBD: When there is no pre/post contract and body, no warnings. *)
if dsp.ds_pre = [] && dsp.ds_post = [] && Ity.Mxs.is_empty dsp.ds_xpost &&
eff_reads = None then
()
else begin
let aggregate_post res_var fvars_uc post =
(* Calculate free vars of postconditions list *)
List.fold_left
(fun (res_var, fvars_uc) (v,t) ->
(* Do not collect result variables of type unit: they can be unused *)
let res_var = if Ity.ity_equal Ity.ity_unit v.pv_ity then res_var
else v :: res_var in
(res_var, t_freevars fvars_uc t))
(res_var, fvars_uc) post in
(* Generate freevars of (x)postconditions before the rest *)
let res_var, fvars_uc_post =
aggregate_post [] Mvs.empty dsp.ds_post in
(* Collect exceptional postcondition freevars and result vars *)
let res_var, fvars_uc_post =
Mxs.fold (fun _ xposts (res_var, fvars_uc) ->
aggregate_post res_var fvars_uc xposts) dsp.ds_xpost (res_var, fvars_uc_post)
in
(* Collect preconditions freevars *)
let fvars_uc = List.fold_left t_freevars fvars_uc_post dsp.ds_pre in
(* Add variables that are marked read by the function. Those are considered
used in particular when we only have the spec of a function. *)
let fvars_uc =
List.fold_left (fun fvars_uc pv -> Mvs.add pv.pv_vs 1 fvars_uc)
fvars_uc dsp.ds_reads in
(* Add terms that are marked writes *)
let fvars_uc =
List.fold_left t_freevars fvars_uc dsp.ds_writes in
(* Add variables used in the body of the function (if there is one) *)
let fvars_uc =
Opt.fold (fun fvars_uc eff ->
List.fold_left (fun fvars_uc pv -> Mvs.add pv.pv_vs 1 fvars_uc)
fvars_uc eff) fvars_uc eff_reads in
let check_present pv = Mvs.mem pv.pv_vs fvars_uc in
let check_used pv =
try check_used_gen ~check_present pv with
| Unused (loc, msg) -> Warning.emit ?loc "%s" msg
let aggregate_post res_var fvars_uc post =
(* Calculate free vars of postconditions list *)
List.fold_left
(fun (res_var, fvars_uc) (v,t) ->
(* Do not collect result variables of type unit: they can be unused *)
let res_var = if Ity.ity_equal Ity.ity_unit v.pv_ity then res_var
else v :: res_var in
(res_var, t_freevars fvars_uc t))
(res_var, fvars_uc) post in
(* Generate freevars of (x)postconditions before the rest *)
let res_var, fvars_uc_post =
aggregate_post [] Mvs.empty dsp.ds_post in
(* Collect exceptional postcondition freevars and result vars *)
let res_var, fvars_uc_post =
Mxs.fold (fun _ xposts (res_var, fvars_uc) ->
aggregate_post res_var fvars_uc xposts) dsp.ds_xpost (res_var, fvars_uc_post)
in
(* Collect preconditions freevars *)
let fvars_uc = List.fold_left t_freevars fvars_uc_post dsp.ds_pre in
(* Add variables that are marked read by the function. Those are considered
used in particular when we only have the spec of a function. *)
let fvars_uc =
List.fold_left (fun fvars_uc pv -> Mvs.add pv.pv_vs 1 fvars_uc)
fvars_uc dsp.ds_reads in
(* Add terms that are marked writes *)
let fvars_uc =
List.fold_left t_freevars fvars_uc dsp.ds_writes in
(* Add variables used in the body of the function (if there is one) *)
let fvars_uc =
Opt.fold (fun fvars_uc eff ->
List.fold_left (fun fvars_uc pv -> Mvs.add pv.pv_vs 1 fvars_uc)
fvars_uc eff) fvars_uc eff_reads in
let check_present pv = Mvs.mem pv.pv_vs fvars_uc in
let check_used pv =
try check_used_gen ~check_present pv with
| Unused (loc, msg) -> Warning.emit ?loc "%s" msg
in
(* Check the usage of normal arguments *)
List.iter check_used bl;
(* The case is different for result variables of postcondition. Those can
occur only in postconditions but each "post" is newly quantified on a
new result variable. In this case, we report an unused variables only if
all the generated result variables are unused. *)
try
let unused =
List.fold_left (fun _ pv ->
(* Exit if we find a result variable that is used *)
try check_used_gen ~check_present pv; raise Exit with
| Unused (loc, msg) -> Some (loc, msg)) None res_var
in
(* Check the usage of normal arguments *)
List.iter check_used bl;
(* The case is different for result variables of postcondition. Those can
occur only in postconditions but each "post" is newly quantified on a
new result variable. In this case, we report an unused variables only if
all the generated result variables are unused. *)
try
let unused =
List.fold_left (fun _ pv ->
(* Exit if we find a result variable that is used *)
try check_used_gen ~check_present pv; raise Exit with
| Unused (loc, msg) -> Some (loc, msg)) None res_var
in
match unused with
| Some (loc, msg) when loc <> None
(* loc = None not supported for results *) -> Warning.emit ?loc "%s" msg
| _ -> ()
with Exit -> ()
end
match unused with
| Some (loc, msg) when loc <> None
(* loc = None not supported for results *) -> Warning.emit ?loc "%s" msg
| _ -> ()
with Exit -> ()
(** Abstract values *)
......
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