diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 75b549f10..1205bceef 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -340,42 +340,38 @@ let store_cfg_to_file source_file::source_file (filename: DB.filename) (cfg: cfg /** clone a procedure description and apply the type substitutions where the parameters are used */ -let specialize_types_proc callee_pdesc resolved_pdesc resolved_formals => { +let specialize_types_proc callee_pdesc resolved_pdesc substitutions => { let resolved_pname = Procdesc.get_proc_name resolved_pdesc and callee_start_node = Procdesc.get_start_node callee_pdesc and callee_exit_node = Procdesc.get_exit_node callee_pdesc; let convert_pvar pvar => Pvar.mk (Pvar.get_name pvar) resolved_pname; + let mk_ptr_typ typename => + /* Only consider pointers from Java objects for now */ + Typ.Tptr (Typ.Tstruct typename) Typ.Pk_pointer; let convert_exp = fun | Exp.Lvar origin_pvar => Exp.Lvar (convert_pvar origin_pvar) | exp => exp; - let extract_class_name = - fun - | Typ.Tptr (Tstruct name) _ => Typename.name name - | _ => failwith "Expecting classname for Java types"; let subst_map = ref Ident.IdentMap.empty; - let redirected_class_name origin_id => + let redirect_typename origin_id => try (Some (Ident.IdentMap.find origin_id !subst_map)) { | Not_found => None }; let convert_instr instrs => fun - | Sil.Load id (Exp.Lvar origin_pvar as origin_exp) origin_typ loc => { - let (_, specialized_typ) = { - let pvar_name = Pvar.get_name origin_pvar; - try (IList.find (fun (n, _) => Mangled.equal n pvar_name) resolved_formals) { - | Not_found => (pvar_name, origin_typ) - } - }; - subst_map := Ident.IdentMap.add id specialized_typ !subst_map; - [Sil.Load id (convert_exp origin_exp) specialized_typ loc, ...instrs] + | Sil.Load + id (Exp.Lvar origin_pvar as origin_exp) (Typ.Tptr (Typ.Tstruct origin_typename) _) loc => { + let specialized_typname = + try (Mangled.Map.find (Pvar.get_name origin_pvar) substitutions) { + | Not_found => origin_typename + }; + subst_map := Ident.IdentMap.add id specialized_typname !subst_map; + [Sil.Load id (convert_exp origin_exp) (mk_ptr_typ specialized_typname) loc, ...instrs] } | Sil.Load id (Exp.Var origin_id as origin_exp) origin_typ loc => { let updated_typ = - switch (Ident.IdentMap.find origin_id !subst_map) { - | Typ.Tptr typ _ => typ - | _ => failwith "Expecting a pointer type" - | exception Not_found => origin_typ + try (mk_ptr_typ (Ident.IdentMap.find origin_id !subst_map)) { + | Not_found => origin_typ }; [Sil.Load id (convert_exp origin_exp) updated_typ loc, ...instrs] } @@ -394,12 +390,13 @@ let specialize_types_proc callee_pdesc resolved_pdesc resolved_formals => { [(Exp.Var id, _), ...origin_args] loc call_flags - when call_flags.CallFlags.cf_virtual && redirected_class_name id != None => { - let redirected_typ = Option.value_exn (redirected_class_name id); + when call_flags.CallFlags.cf_virtual && redirect_typename id != None => { + let redirected_typename = Option.value_exn (redirect_typename id); + let redirected_typ = mk_ptr_typ redirected_typename; let redirected_pname = Procname.replace_class - (Procname.Java callee_pname_java) (extract_class_name redirected_typ) - and args = { + (Procname.Java callee_pname_java) (Typename.name redirected_typename); + let args = { let other_args = IList.map (fun (exp, typ) => (convert_exp exp, typ)) origin_args; [(Exp.Var id, redirected_typ), ...other_args] }; @@ -471,22 +468,23 @@ let specialize_types_proc callee_pdesc resolved_pdesc resolved_formals => { The virtual calls are also replaced to match the parameter types */ let specialize_types callee_pdesc resolved_pname args => { let callee_attributes = Procdesc.get_attributes callee_pdesc; - let resolved_formals = - IList.map2 + let (resolved_params, substitutions) = + IList.fold_left2 ( - fun (param_name, param_typ) (_, arg_typ) => + fun (params, subts) (param_name, param_typ) (_, arg_typ) => switch arg_typ { - | Typ.Tptr (Tstruct _) _ => + | Typ.Tptr (Tstruct typename) Pk_pointer => /* Replace the type of the parameter by the type of the argument */ - (param_name, arg_typ) - | _ => (param_name, param_typ) + ([(param_name, arg_typ), ...params], Mangled.Map.add param_name typename subts) + | _ => ([(param_name, param_typ), ...params], subts) } ) + ([], Mangled.Map.empty) callee_attributes.formals args; let resolved_attributes = { ...callee_attributes, - formals: resolved_formals, + formals: IList.rev resolved_params, proc_name: resolved_pname }; AttributesTable.store_attributes resolved_attributes; @@ -494,5 +492,5 @@ let specialize_types callee_pdesc resolved_pname args => { let tmp_cfg = create_cfg (); create_proc_desc tmp_cfg resolved_attributes }; - specialize_types_proc callee_pdesc resolved_pdesc resolved_formals + specialize_types_proc callee_pdesc resolved_pdesc substitutions }; diff --git a/infer/tests/build_systems/ant/issues.exp b/infer/tests/build_systems/ant/issues.exp index fdfe62cad..c6871500c 100644 --- a/infer/tests/build_systems/ant/issues.exp +++ b/infer/tests/build_systems/ant/issues.exp @@ -106,7 +106,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions. codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor(), 7, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFaillingResourceConstructor(), 6, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFaillingResourceConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionInArrayLengthLoop(java.lang.Object[]), 3, NULL_DEREFERENCE, [start of procedure nullPointerExceptionInArrayLengthLoop(...),Taking true branch] -codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),return from a call to Object NullPointerExceptions.id_generics(NullPointerExceptions$A),return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.(NullPointerExceptions),Taking true branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullArrayParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullArrayParameter(),start of procedure expectNotNullArrayParameter(...)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullObjectParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullObjectParameter(),start of procedure expectNotNullObjectParameter(...)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullableFieldNPE(), 1, NULL_DEREFERENCE, [start of procedure nullableFieldNPE()] @@ -169,7 +169,6 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResources(), codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesRandomAccessFile(), 10, RESOURCE_LEAK, [start of procedure twoResourcesRandomAccessFile(),Taking true branch,exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesServerSocket(), 10, RESOURCE_LEAK, [start of procedure twoResourcesServerSocket(),Taking true branch,exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.zipFileLeakExceptionalBranch(), 5, RESOURCE_LEAK, [start of procedure zipFileLeakExceptionalBranch(),exception java.io.IOException,Switch condition is true. Entering switch case] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory), 9, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketIgnoreExceptionNoVerify(...),start of procedure throwExceptionIfNoVerify(...),Taking true branch,exception javax.net.ssl.SSLException,return from a call to void TaintExample.throwExceptionIfNoVerify(SSLSocket,String),Switch condition is true. Entering switch case] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketNotVerifiedSimple(...)] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession), 7, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketVerifiedForgotToCheckRetval(...)] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.taintingShouldNotPreventInference1(SSLSocketFactory), 4, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure taintingShouldNotPreventInference1(...),start of procedure socketNotVerifiedSimple(...),return from a call to InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory)] diff --git a/infer/tests/build_systems/buck/issues.exp b/infer/tests/build_systems/buck/issues.exp index e9ecf2013..5f015a21f 100644 --- a/infer/tests/build_systems/buck/issues.exp +++ b/infer/tests/build_systems/buck/issues.exp @@ -106,7 +106,7 @@ infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointe infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor(), 7, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFaillingResourceConstructor(), 6, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFaillingResourceConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionInArrayLengthLoop(java.lang.Object[]), 3, NULL_DEREFERENCE, [start of procedure nullPointerExceptionInArrayLengthLoop(...),Taking true branch] -infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),return from a call to Object NullPointerExceptions.id_generics(NullPointerExceptions$A),return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch] +infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.(NullPointerExceptions),Taking true branch] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullArrayParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullArrayParameter(),start of procedure expectNotNullArrayParameter(...)] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullObjectParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullObjectParameter(),start of procedure expectNotNullObjectParameter(...)] infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullableFieldNPE(), 1, NULL_DEREFERENCE, [start of procedure nullableFieldNPE()] @@ -169,7 +169,6 @@ infer/tests/codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoR infer/tests/codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesRandomAccessFile(), 10, RESOURCE_LEAK, [start of procedure twoResourcesRandomAccessFile(),Taking true branch,exception java.io.IOException] infer/tests/codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesServerSocket(), 10, RESOURCE_LEAK, [start of procedure twoResourcesServerSocket(),Taking true branch,exception java.io.IOException] infer/tests/codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.zipFileLeakExceptionalBranch(), 5, RESOURCE_LEAK, [start of procedure zipFileLeakExceptionalBranch(),exception java.io.IOException,Switch condition is true. Entering switch case] -infer/tests/codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory), 9, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketIgnoreExceptionNoVerify(...),start of procedure throwExceptionIfNoVerify(...),Taking true branch,exception javax.net.ssl.SSLException,return from a call to void TaintExample.throwExceptionIfNoVerify(SSLSocket,String),Switch condition is true. Entering switch case] infer/tests/codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketNotVerifiedSimple(...)] infer/tests/codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession), 7, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketVerifiedForgotToCheckRetval(...)] infer/tests/codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.taintingShouldNotPreventInference1(SSLSocketFactory), 4, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure taintingShouldNotPreventInference1(...),start of procedure socketNotVerifiedSimple(...),return from a call to InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory)] diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index 1c86f29ad..9ba4f0f66 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -184,7 +184,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions. codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor(), 7, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFaillingResourceConstructor(), 6, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFaillingResourceConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionInArrayLengthLoop(java.lang.Object[]), 3, NULL_DEREFERENCE, [start of procedure nullPointerExceptionInArrayLengthLoop(...),Taking true branch] -codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),return from a call to Object NullPointerExceptions.id_generics(NullPointerExceptions$A),return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch] +codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.(NullPointerExceptions),Taking true branch] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullArrayParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullArrayParameter(),start of procedure expectNotNullArrayParameter(...)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullObjectParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullObjectParameter(),start of procedure expectNotNullObjectParameter(...)] codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullableFieldNPE(), 1, NULL_DEREFERENCE, [start of procedure nullableFieldNPE()] @@ -231,6 +231,7 @@ codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.fileOutputStreamT codetoanalyze/java/infer/ResourceLeaks.java, int ResourceLeaks.readConfigNotCloseStream(String), 5, RESOURCE_LEAK, [start of procedure readConfigNotCloseStream(...)] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.NoResourceLeakWarningAfterCheckState(File,int), 2, PRECONDITION_NOT_MET, [start of procedure NoResourceLeakWarningAfterCheckState(...),Taking false branch] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.activityObtainTypedArrayAndLeak(Activity), 2, RESOURCE_LEAK, [start of procedure activityObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(Object)] +codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.closeWithCloseablesNestedAlloc(), 5, PRECONDITION_NOT_MET, [start of procedure closeWithCloseablesNestedAlloc()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.closedQuietlyWithCloseables(), 3, RETURN_VALUE_IGNORED, [start of procedure closedQuietlyWithCloseables()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.closedWithCloseables(), 3, RETURN_VALUE_IGNORED, [start of procedure closedWithCloseables()] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.contextObtainTypedArrayAndLeak(Context), 2, RESOURCE_LEAK, [start of procedure contextObtainTypedArrayAndLeak(...),start of procedure ignore(...),return from a call to void ResourceLeaks.ignore(Object)] @@ -287,10 +288,11 @@ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesServ codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.twoResourcesServerSocket(), 10, RESOURCE_LEAK, [start of procedure twoResourcesServerSocket(),Taking true branch,exception java.io.IOException] codetoanalyze/java/infer/ResourceLeaks.java, void ResourceLeaks.zipFileLeakExceptionalBranch(), 5, RESOURCE_LEAK, [start of procedure zipFileLeakExceptionalBranch(),exception java.io.IOException,Switch condition is true. Entering switch case] codetoanalyze/java/infer/ReturnValueIgnored.java, void ReturnValueIgnored.returnValueIgnored(), 1, RETURN_VALUE_IGNORED, [start of procedure returnValueIgnored()] -codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory), 9, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketIgnoreExceptionNoVerify(...),start of procedure throwExceptionIfNoVerify(...),Taking true branch,exception javax.net.ssl.SSLException,return from a call to void TaintExample.throwExceptionIfNoVerify(SSLSocket,String),Switch condition is true. Entering switch case] +codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory), 3, CLASS_CAST_EXCEPTION, [start of procedure socketIgnoreExceptionNoVerify(...)] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketNotVerifiedSimple(...)] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession), 6, RETURN_VALUE_IGNORED, [start of procedure socketVerifiedForgotToCheckRetval(...)] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession), 7, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure socketVerifiedForgotToCheckRetval(...)] +codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.socketVerifiedOk2(SSLSocketFactory), 1, CLASS_CAST_EXCEPTION, [start of procedure socketVerifiedOk2(...)] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.taintingShouldNotPreventInference1(SSLSocketFactory), 4, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure taintingShouldNotPreventInference1(...),start of procedure socketNotVerifiedSimple(...),return from a call to InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory)] codetoanalyze/java/infer/TaintExample.java, InputStream TaintExample.taintingShouldNotPreventInference2(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure taintingShouldNotPreventInference2(...),start of procedure callReadInputStreamCauseTaintError(...),start of procedure readInputStream(...),return from a call to InputStream TaintExample.readInputStream(Socket),return from a call to Socket TaintExample.callReadInputStreamCauseTaintError(SSLSocketFactory)] codetoanalyze/java/infer/TaintExample.java, Socket TaintExample.callReadInputStreamCauseTaintError(SSLSocketFactory), 3, TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION, [start of procedure callReadInputStreamCauseTaintError(...)]