no longer report NULL_TEST_AFTER_DEREFERENCE in tracing mode

Summary:public
In tracing mode, we translate the runtime checks done by the JVM, so the checks for null happen independently from the what happens before the dereference.

Reviewed By: cristianoc

Differential Revision: D2981515

fb-gh-sync-id: 695de07
shipit-source-id: 695de07
master
jrm 9 years ago committed by Facebook Github Bot 1
parent fcd0379d52
commit 8ce56968d6

@ -1073,7 +1073,8 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path
let exn = Exceptions.Bad_pointer_comparison (desc, __POS__) in
Reporting.log_warning pname exn
| _ -> () in
check_already_dereferenced pname cond _prop;
if not !Config.report_runtime_exceptions then
check_already_dereferenced pname cond _prop;
check_condition_always_true_false ();
let n_cond, prop = exp_norm_check_arith pname _prop cond in
ret_old_path (Propset.to_proplist (prune_prop n_cond prop))

Loading…
Cancel
Save