Move the npes regarding smart pointers from B5 to B1.

Reviewed By: akotulski

Differential Revision: D3196759

fb-gh-sync-id: 937efc7
fbshipit-source-id: 937efc7
master
Dulma Churchill 9 years ago committed by Facebook Github Bot 7
parent 442cf66fdc
commit f88e5be395

@ -795,6 +795,7 @@ type inst =
| Itaint
| Iupdate of zero_flag * null_case_flag * int * path_pos
| Ireturn_from_call of int
| Ireturn_from_pointer_wrapper_call of int
(** structured expressions represent a value of structured type, such as an array or a struct. *)
type strexp =
@ -2456,6 +2457,7 @@ let inst_new_loc loc inst = match inst with
| Itaint -> inst
| Iupdate (zf, ncf, _, pos) -> Iupdate (zf, ncf, loc.Location.line, pos)
| Ireturn_from_call _ -> Ireturn_from_call loc.Location.line
| Ireturn_from_pointer_wrapper_call _ -> Ireturn_from_pointer_wrapper_call loc.Location.line
(** return a string representing the inst *)
let inst_to_string inst =
@ -2480,6 +2482,7 @@ let inst_to_string inst =
| Iupdate (zf, ncf, n, _) ->
"update:" ^ zero_flag_to_string zf ^ null_case_flag_to_string ncf ^ string_of_int n
| Ireturn_from_call n -> "return_from_call: " ^ string_of_int n
| Ireturn_from_pointer_wrapper_call n -> "Ireturn_from_pointer_wrapper_call: " ^ string_of_int n
(** join of instrumentations *)
let inst_partial_join inst1 inst2 =
@ -2511,7 +2514,8 @@ let inst_zero_flag = function
| Irearrange (zf, _, _, _) -> zf
| Itaint -> None
| Iupdate (zf, _, _, _) -> zf
| Ireturn_from_call _ -> None
| Ireturn_from_call _
| Ireturn_from_pointer_wrapper_call _ -> None
(** Set the null case flag of the inst. *)
let inst_set_null_case_flag = function
@ -2554,6 +2558,7 @@ let update_inst inst_old inst_new =
let zf' = combine_zero_flags (inst_zero_flag inst_old) zf in
Iupdate (zf', ncf, n, pos)
| Ireturn_from_call _ -> inst_new
| Ireturn_from_pointer_wrapper_call _ -> inst_new
(** describe an instrumentation with a string *)
let pp_inst pe f inst =

@ -450,6 +450,7 @@ type inst =
| Itaint
| Iupdate of zero_flag * null_case_flag * int * path_pos
| Ireturn_from_call of int
| Ireturn_from_pointer_wrapper_call of int
val inst_abstraction : inst
val inst_actual_precondition : inst

@ -115,6 +115,8 @@ let check_access access_opt de_opt =
find_bucket n ncf
| Some (Localise.Returned_from_call n) ->
find_bucket n false
| Some (Localise.Returned_from_pointer_wrapper_call _) ->
Some Localise.BucketLevel.b2
| Some (Localise.Last_accessed (_, is_nullable)) when is_nullable ->
Some Localise.BucketLevel.b1
| _ ->

@ -15,6 +15,24 @@ open! Utils
module L = Logging
module F = Format
let pointer_wrapper_classes = [
["std"; "shared_ptr"];
["std"; "unique_ptr"]
]
let is_pointer_wrapper_class class_name =
IList.exists (fun wrapper_class ->
IList.for_all (fun wrapper_class_substring ->
Utils.string_contains wrapper_class_substring class_name) wrapper_class)
pointer_wrapper_classes
let method_of_pointer_wrapper pname =
match pname with
| Procname.ObjC_Cpp name ->
let class_name = Procname.objc_cpp_get_class_name name in
is_pointer_wrapper_class class_name
| _ -> false
(** Check whether the hpred is a |-> representing a resource in the Racquire state *)
let hpred_is_open_resource prop = function
| Sil.Hpointsto(e, _, _) ->
@ -738,6 +756,10 @@ let explain_dexp_access prop dexp is_nullable =
| Sil.Cfun _ -> (* Treat function as an update *)
Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_call loc.Location.line))
| _ -> None)
| Sil.Dretcall (Sil.Dconst (Sil.Cfun pname as c ) , _, loc, _ )
when method_of_pointer_wrapper pname ->
if !verbose then (L.d_strln "lookup: found Dretcall ");
Some (Sil.Eexp (Sil.Const c, Sil.Ireturn_from_pointer_wrapper_call loc.Location.line))
| de ->
if !verbose then (L.d_strln ("lookup: unknown case not matched " ^ Sil.dexp_to_string de));
None in
@ -753,6 +775,8 @@ let explain_dexp_access prop dexp is_nullable =
Some (Localise.Last_accessed (n, is_nullable))
| Some (Sil.Ireturn_from_call n) ->
Some (Localise.Returned_from_call n)
| Some (Sil.Ireturn_from_pointer_wrapper_call n) ->
Some (Localise.Returned_from_pointer_wrapper_call n)
| Some Sil.Ialloc when !Config.curr_language = Config.Java ->
Some Localise.Initialized_automatically
| Some inst ->

@ -464,6 +464,7 @@ type access =
| Last_accessed of int * bool (* line, is_nullable flag *)
| Initialized_automatically
| Returned_from_call of int
| Returned_from_pointer_wrapper_call of int
let dereference_string deref_str value_str access_opt loc =
let tags = deref_str.tags in
@ -489,6 +490,7 @@ let dereference_string deref_str value_str access_opt loc =
Tags.add tags Tags.assigned_line line_str;
["last assigned on line " ^ line_str]
| Some (Returned_from_call _) -> []
| Some (Returned_from_pointer_wrapper_call _) -> []
| Some Initialized_automatically ->
["initialized automatically"] in
let problem_desc =

@ -171,6 +171,7 @@ type access =
| Last_accessed of int * bool (* line, is_nullable flag *)
| Initialized_automatically
| Returned_from_call of int
| Returned_from_pointer_wrapper_call of int
val dereference_string : deref_str -> string -> access option -> Location.t -> error_desc

Loading…
Cancel
Save