|
|
@ -42,7 +42,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
module CFG = CFG
|
|
|
|
module CFG = CFG
|
|
|
|
module Domain = RecordDomain
|
|
|
|
module Domain = RecordDomain
|
|
|
|
|
|
|
|
|
|
|
|
let report message loc summary =
|
|
|
|
let report var loc summary =
|
|
|
|
|
|
|
|
let message = F.asprintf "The value read from %a was never initialized" Var.pp var in
|
|
|
|
let issue_id = IssueType.uninitialized_value.unique_id in
|
|
|
|
let issue_id = IssueType.uninitialized_value.unique_id in
|
|
|
|
let ltr = [Errlog.make_trace_element 0 loc "" []] in
|
|
|
|
let ltr = [Errlog.make_trace_element 0 loc "" []] in
|
|
|
|
let exn = Exceptions.Checkers (issue_id, Localise.verbatim_desc message) in
|
|
|
|
let exn = Exceptions.Checkers (issue_id, Localise.verbatim_desc message) in
|
|
|
@ -51,6 +52,27 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
|
|
|
|
|
|
|
|
type extras = FormalMap.t * Specs.summary
|
|
|
|
type extras = FormalMap.t * Specs.summary
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let should_report_var pdesc uninit_vars var =
|
|
|
|
|
|
|
|
match var with
|
|
|
|
|
|
|
|
| Var.ProgramVar pv ->
|
|
|
|
|
|
|
|
not (Pvar.is_frontend_tmp pv) && not (Procdesc.is_captured_var pdesc pv)
|
|
|
|
|
|
|
|
&& exp_in_set (Exp.Lvar pv) uninit_vars
|
|
|
|
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
false
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let report_on_function_params pdesc uninit_vars actuals loc extras =
|
|
|
|
|
|
|
|
List.iter
|
|
|
|
|
|
|
|
~f:(fun e ->
|
|
|
|
|
|
|
|
match e with
|
|
|
|
|
|
|
|
| HilExp.AccessPath ((var, t), _)
|
|
|
|
|
|
|
|
when should_report_var pdesc uninit_vars var && not (is_type_pointer t) ->
|
|
|
|
|
|
|
|
report var loc (snd extras)
|
|
|
|
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
())
|
|
|
|
|
|
|
|
actuals
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let exec_instr (astate: Domain.astate) {ProcData.pdesc; ProcData.extras} _ (instr: HilInstr.t) =
|
|
|
|
let exec_instr (astate: Domain.astate) {ProcData.pdesc; ProcData.extras} _ (instr: HilInstr.t) =
|
|
|
|
match instr with
|
|
|
|
match instr with
|
|
|
|
| Assign (((lhs_var, lhs_typ), _), HilExp.AccessPath (((rhs_var, rhs_typ) as rhs_base), _), loc) ->
|
|
|
|
| Assign (((lhs_var, lhs_typ), _), HilExp.AccessPath (((rhs_var, rhs_typ) as rhs_base), _), loc) ->
|
|
|
@ -64,21 +86,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
(pre', post)
|
|
|
|
(pre', post)
|
|
|
|
else astate.prepost
|
|
|
|
else astate.prepost
|
|
|
|
in
|
|
|
|
in
|
|
|
|
( match rhs_var with
|
|
|
|
(* check on lhs_typ to avoid false positive when assigning a pointer to another *)
|
|
|
|
| Var.ProgramVar pv
|
|
|
|
if should_report_var pdesc uninit_vars rhs_var && not (is_type_pointer lhs_typ) then
|
|
|
|
when not (Pvar.is_frontend_tmp pv) && not (Procdesc.is_captured_var pdesc pv)
|
|
|
|
report rhs_var loc (snd extras) ;
|
|
|
|
&& exp_in_set (Exp.Lvar pv) uninit_vars && not (is_type_pointer lhs_typ) ->
|
|
|
|
|
|
|
|
let message =
|
|
|
|
|
|
|
|
F.asprintf "The value read from %a was never initialized" Exp.pp (Exp.Lvar pv)
|
|
|
|
|
|
|
|
in
|
|
|
|
|
|
|
|
report message loc (snd extras)
|
|
|
|
|
|
|
|
| _ ->
|
|
|
|
|
|
|
|
() ) ;
|
|
|
|
|
|
|
|
{astate with uninit_vars; prepost}
|
|
|
|
{astate with uninit_vars; prepost}
|
|
|
|
| Assign (((lhs_var, _), _), _, _) ->
|
|
|
|
| Assign (((lhs_var, _), _), _, _) ->
|
|
|
|
let uninit_vars = D.remove lhs_var astate.uninit_vars in
|
|
|
|
let uninit_vars = D.remove lhs_var astate.uninit_vars in
|
|
|
|
{astate with uninit_vars}
|
|
|
|
{astate with uninit_vars}
|
|
|
|
| Call (_, _, actuals, _, _) ->
|
|
|
|
| Call (_, _, actuals, _, loc) ->
|
|
|
|
(* in case of intraprocedural only analysis we assume that parameters passed by reference
|
|
|
|
(* in case of intraprocedural only analysis we assume that parameters passed by reference
|
|
|
|
to a function will be initialized inside that function *)
|
|
|
|
to a function will be initialized inside that function *)
|
|
|
|
let uninit_vars =
|
|
|
|
let uninit_vars =
|
|
|
@ -88,12 +103,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
|
|
|
|
| HilExp.AccessPath ((actual_var, {Typ.desc= Tptr _}), _) ->
|
|
|
|
| HilExp.AccessPath ((actual_var, {Typ.desc= Tptr _}), _) ->
|
|
|
|
D.remove actual_var acc
|
|
|
|
D.remove actual_var acc
|
|
|
|
| HilExp.Closure (_, apl) ->
|
|
|
|
| HilExp.Closure (_, apl) ->
|
|
|
|
(* remove the captured variables of a block *)
|
|
|
|
(* remove the captured variables of a block/lambda *)
|
|
|
|
List.fold ~f:(fun acc' ((av, _), _) -> D.remove av acc') ~init:acc apl
|
|
|
|
List.fold ~f:(fun acc' ((av, _), _) -> D.remove av acc') ~init:acc apl
|
|
|
|
| _ ->
|
|
|
|
| _ ->
|
|
|
|
acc)
|
|
|
|
acc)
|
|
|
|
~init:astate.uninit_vars actuals
|
|
|
|
~init:astate.uninit_vars actuals
|
|
|
|
in
|
|
|
|
in
|
|
|
|
|
|
|
|
report_on_function_params pdesc uninit_vars actuals loc extras ;
|
|
|
|
{astate with uninit_vars}
|
|
|
|
{astate with uninit_vars}
|
|
|
|
| Assume _ ->
|
|
|
|
| Assume _ ->
|
|
|
|
astate
|
|
|
|
astate
|
|
|
|