@ -608,29 +608,30 @@ let forward_tabulate cfg tenv =
done ;
done ;
L . d_strln " .... Work list empty. Stop .... " ; L . d_ln ()
L . d_strln " .... Work list empty. Stop .... " ; L . d_ln ()
(* * report an error if any Activity is reachable from a static field *)
let report_activity_leaks pname sigma tenv =
(* * report an error if any Context is reachable from a static field *)
(* report an error if an expression in [activity_exps] is reachable from [field_strexp] *)
let report_context_leaks pname sigma tenv =
let check_reachable_activity_from_fld ( fld_name , fld_strexp ) activity_exps =
(* report an error if an expression in [context_exps] is reachable from [field_strexp] *)
let check_reachable_context_from_fld ( fld_name , fld_strexp ) context_exps =
let fld_exps = Prop . strexp_get_exps fld_strexp in
let fld_exps = Prop . strexp_get_exps fld_strexp in
let reachable_hpreds , reachable_exps =
let reachable_hpreds , reachable_exps =
Prop . compute_reachable_hpreds sigma fld_exps in
Prop . compute_reachable_hpreds sigma fld_exps in
(* raise an error if any Activity expression is in [reachable_exps] *)
(* raise an error if any Context expression is in [reachable_exps] *)
IList . iter
IList . iter
( fun ( activity _exp, typ ) ->
( fun ( context _exp, typ ) ->
if Sil . ExpSet . mem activity _exp reachable_exps then
if Sil . ExpSet . mem context _exp reachable_exps then
let leak_path = Prop . get_fld_typ_path fld_exps activity _exp reachable_hpreds in
let leak_path = Prop . get_fld_typ_path fld_exps context _exp reachable_hpreds in
let err_desc = Errdesc . explain_ activity _leak pname typ fld_name leak_path in
let err_desc = Errdesc . explain_ context _leak pname typ fld_name leak_path in
let exn = Exceptions . Activity _leak
let exn = Exceptions . Context _leak
( err_desc , try assert false with Assert_failure x -> x ) in
( err_desc , try assert false with Assert_failure x -> x ) in
Reporting . log_error pname exn )
Reporting . log_error pname exn )
activity _exps in
context _exps in
(* get the set of pointed-to expressions of type T <: Activity *)
(* get the set of pointed-to expressions of type T <: Context *)
let activity _exps =
let context _exps =
IList . fold_left
IList . fold_left
( fun exps hpred -> match hpred with
( fun exps hpred -> match hpred with
| Sil . Hpointsto ( _ , Sil . Eexp ( exp , _ ) , Sil . Sizeof ( Sil . Tptr ( typ , _ ) , _ ) )
| Sil . Hpointsto ( _ , Sil . Eexp ( exp , _ ) , Sil . Sizeof ( Sil . Tptr ( typ , _ ) , _ ) )
when AndroidFramework . is_ activity typ tenv ->
when AndroidFramework . is_ context typ tenv ->
( exp , typ ) :: exps
( exp , typ ) :: exps
| _ -> exps )
| _ -> exps )
[]
[]
@ -641,7 +642,7 @@ let report_activity_leaks pname sigma tenv =
IList . iter
IList . iter
( fun ( f_name , f_strexp ) ->
( fun ( f_name , f_strexp ) ->
if not ( Harness . is_generated_field f_name ) then
if not ( Harness . is_generated_field f_name ) then
check_reachable_ activity_from_fld ( f_name , f_strexp ) activity _exps) static_flds
check_reachable_ context_from_fld ( f_name , f_strexp ) context _exps) static_flds
| _ -> () )
| _ -> () )
sigma
sigma
@ -702,7 +703,7 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
let pre , post = Prop . extract_spec prop'' in
let pre , post = Prop . extract_spec prop'' in
let pre' = Prop . normalize ( Prop . prop_sub sub pre ) in
let pre' = Prop . normalize ( Prop . prop_sub sub pre ) in
if ! Config . curr_language = Config . Java then
if ! Config . curr_language = Config . Java then
report_ activity _leaks pname ( Prop . get_sigma post ) tenv ;
report_ context _leaks pname ( Prop . get_sigma post ) tenv ;
let post' =
let post' =
if Prover . check_inconsistency_base prop then None
if Prover . check_inconsistency_base prop then None
else Some ( Prop . normalize ( Prop . prop_sub sub post ) , path ) in
else Some ( Prop . normalize ( Prop . prop_sub sub post ) , path ) in