|
|
@ -1039,25 +1039,27 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
|
|
|
|
| Sil.Prune (cond, loc, true_branch, ik) ->
|
|
|
|
| Sil.Prune (cond, loc, true_branch, ik) ->
|
|
|
|
let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in
|
|
|
|
let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in
|
|
|
|
let check_condition_always_true_false () =
|
|
|
|
let check_condition_always_true_false () =
|
|
|
|
let report_condition_always_true_false i =
|
|
|
|
if !Config.curr_language <> Config.Clang ||
|
|
|
|
let skip_loop = match ik with
|
|
|
|
Config.report_condition_always_true_in_clang then
|
|
|
|
| Sil.Ik_while | Sil.Ik_for ->
|
|
|
|
let report_condition_always_true_false i =
|
|
|
|
not (IntLit.iszero i) (* skip wile(1) and for (;1;) *)
|
|
|
|
let skip_loop = match ik with
|
|
|
|
| Sil.Ik_dowhile ->
|
|
|
|
| Sil.Ik_while | Sil.Ik_for ->
|
|
|
|
true (* skip do..while *)
|
|
|
|
not (IntLit.iszero i) (* skip wile(1) and for (;1;) *)
|
|
|
|
| Sil.Ik_land_lor ->
|
|
|
|
| Sil.Ik_dowhile ->
|
|
|
|
true (* skip subpart of a condition obtained from compilation of && and || *)
|
|
|
|
true (* skip do..while *)
|
|
|
|
| _ -> false in
|
|
|
|
| Sil.Ik_land_lor ->
|
|
|
|
true_branch && not skip_loop in
|
|
|
|
true (* skip subpart of a condition obtained from compilation of && and || *)
|
|
|
|
match Prop.exp_normalize_prop tenv Prop.prop_emp cond with
|
|
|
|
| _ -> false in
|
|
|
|
| Exp.Const (Const.Cint i) when report_condition_always_true_false i ->
|
|
|
|
true_branch && not skip_loop in
|
|
|
|
let node = State.get_node () in
|
|
|
|
match Prop.exp_normalize_prop tenv Prop.prop_emp cond with
|
|
|
|
let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
|
|
|
|
| Exp.Const (Const.Cint i) when report_condition_always_true_false i ->
|
|
|
|
let exn =
|
|
|
|
let node = State.get_node () in
|
|
|
|
Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) in
|
|
|
|
let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
|
|
|
|
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop current_pname) in
|
|
|
|
let exn =
|
|
|
|
Reporting.log_warning current_pname ?pre:pre_opt exn
|
|
|
|
Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__) in
|
|
|
|
| _ -> () in
|
|
|
|
let pre_opt = State.get_normalized_pre (Abs.abstract_no_symop current_pname) in
|
|
|
|
|
|
|
|
Reporting.log_warning current_pname ?pre:pre_opt exn
|
|
|
|
|
|
|
|
| _ -> () in
|
|
|
|
if not Config.report_runtime_exceptions then
|
|
|
|
if not Config.report_runtime_exceptions then
|
|
|
|
check_already_dereferenced tenv current_pname cond prop__;
|
|
|
|
check_already_dereferenced tenv current_pname cond prop__;
|
|
|
|
check_condition_always_true_false ();
|
|
|
|
check_condition_always_true_false ();
|
|
|
|