diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index b277a3467..5ad85e8bb 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -79,18 +79,6 @@ module Misc = struct PulseOperations.write_id ret_id ret_value astate - let return_zero_prune_positive ~desc (address, hist) : model = - fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> - let event = ValueHistory.Call {f= Model desc; location; in_call= []} in - let fresh_elem = AbstractValue.mk_fresh () in - let<+> astate = - PulseArithmetic.prune_positive address astate - >>= PulseArithmetic.and_eq_int fresh_elem IntLit.zero - >>| PulseOperations.write_id ret_id (fresh_elem, event :: hist) - in - astate - - let return_unknown_size : model = fun _ ~callee_procname:_ _location ~ret:(ret_id, _) astate -> let ret_addr = AbstractValue.mk_fresh () in @@ -996,9 +984,9 @@ module JavaCollection = struct Java.mk_java_field pkg_name class_name "__infer_model_backing_collection_empty" - let init this : model = - fun _ ~callee_procname:_ location ~ret:(_, _) astate -> - let event = ValueHistory.Call {f= Model "Collection."; location; in_call= []} in + let init ~desc this : model = + fun _ ~callee_procname:_ location ~ret:_ astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let fresh_val = (AbstractValue.mk_fresh (), [event]) in let is_empty_value = AbstractValue.mk_fresh () in let init_value = AbstractValue.mk_fresh () in @@ -1017,9 +1005,9 @@ module JavaCollection = struct astate |> ok_continue - let add coll new_elem : model = + let add ~desc coll new_elem : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> - let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let ret_value = AbstractValue.mk_fresh () in let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in (* reads snd_field from collection *) @@ -1047,7 +1035,7 @@ module JavaCollection = struct astate |> ok_continue - let add_at coll (_, _) new_elem : model = add coll new_elem + let add_at ~desc coll _ new_elem : model = add ~desc coll new_elem let update coll new_val new_val_hist event location ret_id astate = (* case0: element not present in collection *) @@ -1071,15 +1059,15 @@ module JavaCollection = struct [astate; astate1; astate2] - let set coll (_, _) (new_val, new_val_hist) : model = + let set coll _ (new_val, new_val_hist) : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> - let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in + let event = ValueHistory.Call {f= Model "Collection.set()"; location; in_call= []} in let<*> astates = update coll new_val new_val_hist event location ret_id astate in List.map ~f:(fun astate -> Ok (ContinueProgram astate)) astates - let remove_at coll location ret_id astate = - let event = ValueHistory.Call {f= Model "Collection.remove"; location; in_call= []} in + let remove_at ~desc coll location ret_id astate = + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let new_val = AbstractValue.mk_fresh () in PulseArithmetic.and_eq_int new_val IntLit.zero astate >>= update coll new_val [] event location ret_id @@ -1111,8 +1099,8 @@ module JavaCollection = struct Ok astate - let remove_obj coll (elem, _) location ret_id astate = - let event = ValueHistory.Call {f= Model "Collection.remove"; location; in_call= []} in + let remove_obj ~desc coll (elem, _) location ret_id astate = + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let* astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in (* case1: given element is equal to fst_field *) let* astate, fst_addr, (fst_val, _) = Java.load_field fst_field location coll_val astate in @@ -1130,7 +1118,7 @@ module JavaCollection = struct [astate1; astate2; astate] - let remove args : model = + let remove ~desc args : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> match args with | [ {ProcnameDispatcher.Call.FuncArg.arg_payload= coll_arg} @@ -1139,29 +1127,29 @@ module JavaCollection = struct match typ.desc with | Tint _ -> (* Case of remove(int index) *) - remove_at coll_arg location ret_id astate + remove_at ~desc coll_arg location ret_id astate | _ -> (* Case of remove(Object o) *) - remove_obj coll_arg elem_arg location ret_id astate + remove_obj ~desc coll_arg elem_arg location ret_id astate in List.map ~f:(fun astate -> Ok (ContinueProgram astate)) astates | _ -> astate |> ok_continue - let is_empty coll : model = + let is_empty ~desc coll : model = fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> - let event = ValueHistory.Call {f= Model "Collection.isEmpty"; location; in_call= []} in + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in - let<*> astate, (_, _), (is_empty_val, hist) = + let<*> astate, _, (is_empty_val, hist) = Java.load_field is_empty_field location coll_val astate in PulseOperations.write_id ret_id (is_empty_val, event :: hist) astate |> ok_continue - let clear coll : model = - fun _ ~callee_procname:_ location ~ret:(_, _) astate -> - let event = ValueHistory.Call {f= Model "Collection.clear"; location; in_call= []} in + let clear ~desc coll : model = + fun _ ~callee_procname:_ location ~ret:_ astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in let null_val = AbstractValue.mk_fresh () in let is_empty_val = AbstractValue.mk_fresh () in let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in @@ -1175,6 +1163,69 @@ module JavaCollection = struct >>= PulseArithmetic.and_eq_int is_empty_val IntLit.one in astate + + + (* Auxiliary function that changes the state by + (1) assuming that internal is_empty field has value one + (2) in such case we can return 0 *) + let get_elem_coll_is_empty is_empty_val is_empty_expected_val event location ret_id astate = + let not_found_val = AbstractValue.mk_fresh () in + let* astate = + PulseArithmetic.prune_binop ~negated:false Binop.Eq (AbstractValueOperand is_empty_val) + (AbstractValueOperand is_empty_expected_val) astate + >>= PulseArithmetic.and_eq_int not_found_val IntLit.zero + >>= PulseArithmetic.and_eq_int is_empty_expected_val IntLit.one + in + let astate = PulseOperations.write_id ret_id (not_found_val, [event]) astate in + PulseOperations.invalidate location (ConstantDereference IntLit.zero) + (not_found_val, [event]) + astate + + + (* Auxiliary function that splits the state into three, considering the case that + the internal is_empty field is not known to have value 1 *) + let get_elem_coll_not_known_empty elem found_val fst_val snd_val astate = + (* case 1: given element is not equal to the fst AND not equal to the snd *) + let* astate1 = + PulseArithmetic.prune_binop ~negated:true Binop.Eq (AbstractValueOperand elem) + (AbstractValueOperand fst_val) astate + >>= PulseArithmetic.prune_binop ~negated:true Binop.Eq (AbstractValueOperand elem) + (AbstractValueOperand snd_val) + in + let* astate = PulseArithmetic.and_positive found_val astate in + (* case 2: given element is equal to fst_field *) + let* astate2 = + PulseArithmetic.prune_binop ~negated:false Binop.Eq (AbstractValueOperand elem) + (AbstractValueOperand fst_val) astate + in + (* case 3: given element is equal to snd_field *) + let+ astate3 = + PulseArithmetic.prune_binop ~negated:false Binop.Eq (AbstractValueOperand elem) + (AbstractValueOperand snd_val) astate + in + [astate1; astate2; astate3] + + + let get ~desc coll (elem, _) : model = + fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate -> + let event = ValueHistory.Call {f= Model desc; location; in_call= []} in + let<*> astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in + let<*> astate, _, (is_empty_val, _) = Java.load_field is_empty_field location coll_val astate in + (* case 1: collection is empty *) + let true_val = AbstractValue.mk_fresh () in + let<*> astate1 = get_elem_coll_is_empty is_empty_val true_val event location ret_id astate in + (* case 2: collection is not known to be empty *) + let found_val = AbstractValue.mk_fresh () in + let<*> astate2, _, (fst_val, _) = Java.load_field fst_field location coll_val astate in + let<*> astate2, _, (snd_val, _) = Java.load_field snd_field location coll_val astate2 in + let<*> astate2 = + PulseArithmetic.prune_binop ~negated:true Binop.Eq (AbstractValueOperand is_empty_val) + (AbstractValueOperand true_val) astate2 + >>= PulseArithmetic.and_eq_int true_val IntLit.one + in + let astate2 = PulseOperations.write_id ret_id (found_val, [event]) astate2 in + let<*> astates = get_elem_coll_not_known_empty elem found_val fst_val snd_val astate2 in + List.map (astate1 :: astates) ~f:(fun astate -> Ok (ContinueProgram astate)) end module JavaInteger = struct @@ -1515,24 +1566,47 @@ module ProcNameDispatcher = struct ; -"std" &:: "vector" &:: "push_back" <>$ capt_arg_payload $+...$--> StdVector.push_back ; -"std" &:: "vector" &:: "empty" <>$ capt_arg_payload $+...$--> StdVector.empty ; +map_context_tenv PatternMatch.Java.implements_collection - &:: "" <>$ capt_arg_payload $--> JavaCollection.init + &:: "" <>$ capt_arg_payload + $--> JavaCollection.init ~desc:"Collection.init()" ; +map_context_tenv PatternMatch.Java.implements_collection - &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $--> JavaCollection.add + &:: "add" <>$ capt_arg_payload $+ capt_arg_payload + $--> JavaCollection.add ~desc:"Collection.add" ; +map_context_tenv PatternMatch.Java.implements_list &:: "add" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload - $--> JavaCollection.add_at + $--> JavaCollection.add_at ~desc:"Collection.add()" ; +map_context_tenv PatternMatch.Java.implements_collection - &:: "remove" &++> JavaCollection.remove + &:: "remove" + &++> JavaCollection.remove ~desc:"Collection.remove" ; +map_context_tenv PatternMatch.Java.implements_collection - &:: "isEmpty" <>$ capt_arg_payload $--> JavaCollection.is_empty + &:: "isEmpty" <>$ capt_arg_payload + $--> JavaCollection.is_empty ~desc:"Collection.isEmpty()" ; +map_context_tenv PatternMatch.Java.implements_collection - &:: "clear" <>$ capt_arg_payload $--> JavaCollection.clear + &:: "clear" <>$ capt_arg_payload + $--> JavaCollection.clear ~desc:"Collection.clear()" ; +map_context_tenv PatternMatch.Java.implements_collection &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "" <>$ capt_arg_payload + $--> JavaCollection.init ~desc:"Map.init()" + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "put" <>$ capt_arg_payload $+ capt_arg_payload + $+...$--> JavaCollection.add ~desc:"Map.put()" + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "remove" + &++> JavaCollection.remove ~desc:"Map.remove()" + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "get" <>$ capt_arg_payload $+ capt_arg_payload + $--> JavaCollection.get ~desc:"Map.get()" + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "containsKey" <>$ capt_arg_payload $+ capt_arg_payload + $--> JavaCollection.get ~desc:"Map.containsKey()" ; +map_context_tenv PatternMatch.Java.implements_map &:: "isEmpty" <>$ capt_arg_payload - $--> Misc.return_zero_prune_positive ~desc:"Map.isEmpty()" + $--> JavaCollection.is_empty ~desc:"Map.isEmpty()" + ; +map_context_tenv PatternMatch.Java.implements_map + &:: "clear" <>$ capt_arg_payload + $--> JavaCollection.clear ~desc:"Map.clear()" ; +map_context_tenv PatternMatch.Java.implements_queue &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back diff --git a/infer/tests/codetoanalyze/java/pulse/HashMapExample.java b/infer/tests/codetoanalyze/java/pulse/HashMapExample.java index 2b1499c6c..9739741d3 100644 --- a/infer/tests/codetoanalyze/java/pulse/HashMapExample.java +++ b/infer/tests/codetoanalyze/java/pulse/HashMapExample.java @@ -11,7 +11,7 @@ import java.util.HashMap; public class HashMapExample { - public static void putIntegerTwiceThenGetTwice(HashMap hashMap) { + public static void putIntegerTwiceThenGetTwiceOk(HashMap hashMap) { Integer i32 = new Integer(32); Integer i52 = new Integer(52); @@ -25,7 +25,7 @@ public class HashMapExample { b.intValue(); } - public static void containsIntegerTwiceThenGetTwice(HashMap hashMap) { + public static void containsIntegerTwiceThenGetTwiceOk(HashMap hashMap) { Integer i32 = new Integer(32); Integer i52 = new Integer(52); @@ -37,7 +37,7 @@ public class HashMapExample { } } - public static int FN_getOneIntegerWithoutCheck() { + public static int getOneIntegerWithoutCheckBad() { HashMap hashMap = new HashMap<>(); Integer i32 = new Integer(32); @@ -46,7 +46,7 @@ public class HashMapExample { return a.intValue(); } - public static void FN_getTwoIntegersWithOneCheck(Integer i, Integer j) { + public static void getTwoIntegersWithOneCheckOk(Integer i, Integer j) { HashMap hashMap = new HashMap<>(); if (hashMap.containsKey(i) && !i.equals(j)) { @@ -69,13 +69,13 @@ public class HashMapExample { return x; } - public static void getOrCreateIntegerThenDeref(final HashMap map) { + public static void getOrCreateIntegerThenDerefOk(final HashMap map) { Integer x = getOrCreateInteger(map, 42); // dereference x x.toString(); } - void FN_getAfterRemovingTheKeyBad() { + void getAfterRemovingTheKeyBad() { HashMap map = new HashMap(); Integer key = 42; map.put(key, new Object()); @@ -91,7 +91,7 @@ public class HashMapExample { map.get(key).toString(); } - void FN_getAfterClearBad() { + void getAfterClearBad() { HashMap map = new HashMap(); Integer key = 42; map.put(key, new Object()); @@ -99,7 +99,10 @@ public class HashMapExample { map.get(key).toString(); // NPE here } - void getFromKeySetGood(HashMap map) { + // A null pointer dereference is currently reported as latent (during the access of + // s.equals("foo")). + // Once keySet() is modelled, this null deference should not be reported anymore + void FP_latent_getFromKeySetOk(HashMap map) { for (String key : map.keySet()) { String s = map.get(key); if (s.equals("foo")) { diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index ec7f14e31..ce46dc44c 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -14,6 +14,10 @@ codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicD codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object DynamicDispatch$Subtype.foo()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object DynamicDispatch$Subtype.foo()`,return from call to `Object DynamicDispatch$Subtype.foo()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicResolutionWithVariadicMethodBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,return from call to `Object DynamicDispatch.variadicMethod(DynamicDispatch$Supertype[])`,assigned,invalid access occurs here] codetoanalyze/java/pulse/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasyBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object DynamicDispatch$Impl.foo()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object DynamicDispatch$Impl.foo()`,return from call to `Object DynamicDispatch$Impl.foo()`,assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.FP_latent_getFromKeySetOk(java.util.HashMap):void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterClearBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getAfterRemovingTheKeyBad():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,invalid access occurs here] +codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getOneIntegerWithoutCheckBad():int, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.checkInstanceArray(java.lang.Object):void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfBooleanArrayBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `void InstanceOfExample.checkInstanceArray(Object)`,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfObjProfessorBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here] @@ -39,12 +43,14 @@ codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.Nu codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_sinkWithNeverNullSource():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `T NeverNullSource.get()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `T NeverNullSource.get()`,return from call to `T NeverNullSource.get()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_stringConstantEqualsTrueNotNPE():void, 12, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.NPEvalueOfFromHashmapBad(java.util.HashMap,int):int, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.badCheckShouldCauseNPE():void, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.getObj()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.getObj()`,return from call to `Object NullPointerExceptions.getObj()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNull():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.derefUndefinedCallee()` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.derefUndefinedCallee()`,return from call to `Object NullPointerExceptions.derefUndefinedCallee()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.nullableRet(boolean)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.nullableRet(boolean)`,return from call to `Object NullPointerExceptions.nullableRet(boolean)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)`,return from call to `Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerException():int, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionArrayLength():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.nullPointerExceptionCallArrayReadMethod():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)`,return from call to `Object NullPointerExceptions.arrayReadShouldNotCauseSymexMemoryError(int)`,assigned,invalid access occurs here]