@ -1121,7 +1121,6 @@ let reachable_when_in_several_hpreds sigma : Ident.t -> bool =
list_iter add_hpred sigma ;
list_iter add_hpred sigma ;
id_in_several_hpreds
id_in_several_hpreds
let full_reachability_algorithm = true
(* Check whether the hidden counter field of a struct representing an *)
(* Check whether the hidden counter field of a struct representing an *)
(* objective-c object is positive, and whether the leak is part of the *)
(* objective-c object is positive, and whether the leak is part of the *)
@ -1230,11 +1229,8 @@ let check_junk ?original_prop pname tenv prop =
let remove_junk_once fp_part fav_root sigma =
let remove_junk_once fp_part fav_root sigma =
let id_considered_reachable = (* reachability function *)
let id_considered_reachable = (* reachability function *)
if full_reachability_algorithm then
let reach_set = sigma_reachable fav_root sigma in
let reach_set = sigma_reachable fav_root sigma in
fun id -> Ident . IdentSet . mem id reach_set
fun id -> Ident . IdentSet . mem id reach_set in
else
reachable_when_in_several_hpreds sigma in
let should_remove_hpred entries =
let should_remove_hpred entries =
let predicate = function
let predicate = function
| Sil . Var id ->
| Sil . Var id ->
@ -1259,16 +1255,14 @@ let check_junk ?original_prop pname tenv prop =
Sil . strexp_fav_add fav se ;
Sil . strexp_fav_add fav se ;
Sil . fav_mem fav id
Sil . fav_mem fav id
| _ -> false in
| _ -> false in
hpred_is_loop
hpred_is_loop | | list_exists predicate entries in
| |
list_exists predicate entries in
let rec remove_junk_recursive sigma_done sigma_todo =
let rec remove_junk_recursive sigma_done sigma_todo =
match sigma_todo with
match sigma_todo with
| [] -> list_rev sigma_done
| [] -> list_rev sigma_done
| hpred :: sigma_todo' ->
| hpred :: sigma_todo' ->
let entries = hpred_entries hpred in
let entries = hpred_entries hpred in
if should_remove_hpred entries
if should_remove_hpred entries then
then begin
begin
let part = if fp_part then " footprint " else " normal " in
let part = if fp_part then " footprint " else " normal " in
L . d_strln ( " .... Prop with garbage in " ^ part ^ " part .... " ) ;
L . d_strln ( " .... Prop with garbage in " ^ part ^ " part .... " ) ;
L . d_increase_indent 1 ;
L . d_increase_indent 1 ;
@ -1277,7 +1271,8 @@ let check_junk ?original_prop pname tenv prop =
L . d_strln " PREDICATE: " ;
L . d_strln " PREDICATE: " ;
Prop . d_sigma [ hpred ] ;
Prop . d_sigma [ hpred ] ;
L . d_ln () ;
L . d_ln () ;
let alloc_attribute = (* find the alloc attribute of one of the roots of hpred, if it exists *)
let alloc_attribute =
(* find the alloc attribute of one of the roots of hpred, if it exists *)
let res = ref None in
let res = ref None in
let do_entry e =
let do_entry e =
match Prop . get_resource_undef_attribute prop e with
match Prop . get_resource_undef_attribute prop e with
@ -1328,8 +1323,6 @@ let check_junk ?original_prop pname tenv prop =
let cycle = get_var_retain_cycle ( remove_opt original_prop ) in
let cycle = get_var_retain_cycle ( remove_opt original_prop ) in
false , exn_retain_cycle cycle
false , exn_retain_cycle cycle
| _ -> ! Sil . curr_language = Sil . Java , exn_leak ) in
| _ -> ! Sil . curr_language = Sil . Java , exn_leak ) in
let ignore_leak = ! Config . allowleak | | ignore_resource | | is_undefined in
let report_and_continue = ! Config . footprint in (* in footprint mode, report leak and continue *)
let already_reported () =
let already_reported () =
let attr_opt_equal ao1 ao2 = match ao1 , ao2 with
let attr_opt_equal ao1 ao2 = match ao1 , ao2 with
| None , None -> true
| None , None -> true
@ -1338,21 +1331,20 @@ let check_junk ?original_prop pname tenv prop =
| None , Some _ -> false in
| None , Some _ -> false in
( alloc_attribute = None && ! leaks_reported < > [] ) | | (* None attribute only reported if it's the first one *)
( alloc_attribute = None && ! leaks_reported < > [] ) | | (* None attribute only reported if it's the first one *)
list_mem attr_opt_equal alloc_attribute ! leaks_reported in
list_mem attr_opt_equal alloc_attribute ! leaks_reported in
let ignore_leak =
! Config . allowleak | | ignore_resource | | is_undefined | | already_reported () in
(* in footprint mode, report leak and continue *)
let report_and_continue = ! Config . footprint in
let report_leak () =
let report_leak () =
if report_and_continue then
if not report_and_continue then raise exn
else
begin
begin
if not ( already_reported () ) (* report each leak only once *)
then begin
Reporting . log_error pname exn ;
Reporting . log_error pname exn ;
Exceptions . print_exception_html " Error: " exn ;
end ;
leaks_reported := alloc_attribute :: ! leaks_reported ;
leaks_reported := alloc_attribute :: ! leaks_reported ;
end in
if not ignore_leak then report_leak () ;
remove_junk_recursive sigma_done sigma_todo'
remove_junk_recursive sigma_done sigma_todo'
end
end
else raise exn in
if ignore_leak then remove_junk_recursive sigma_done sigma_todo'
else report_leak ()
end
else
else
remove_junk_recursive ( hpred :: sigma_done ) sigma_todo' in
remove_junk_recursive ( hpred :: sigma_done ) sigma_todo' in
remove_junk_recursive [] sigma in
remove_junk_recursive [] sigma in