diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 2abe7d738..b277a3467 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1178,19 +1178,11 @@ module JavaCollection = struct end module JavaInteger = struct - let internal_int = - Fieldname.make - (Typ.JavaClass (JavaClassName.make ~package:(Some "java.lang") ~classname:"Integer")) - "__infer_model_backing_int" - + let internal_int = Java.mk_java_field "java.lang" "Integer" "__infer_model_backing_int" let load_backing_int location this astate = let* astate, obj = PulseOperations.eval_access Read location this Dereference astate in - let* astate, int_addr = - PulseOperations.eval_access Read location obj (FieldAccess internal_int) astate - in - let+ astate, int_val = PulseOperations.eval_access Read location int_addr Dereference astate in - (astate, int_addr, int_val) + Java.load_field internal_int location obj astate let construct this_address init_value event location astate = @@ -1202,7 +1194,7 @@ module JavaInteger = struct PulseOperations.write_deref location ~ref:this_address ~obj:this astate - let constructor this_address init_value : model = + let init this_address init_value : model = fun _ ~callee_procname:_ location ~ret:_ astate -> let event = ValueHistory.Call {f= Model "Integer.init"; location; in_call= []} in let<+> astate = construct this_address init_value event location astate in @@ -1554,7 +1546,7 @@ module ProcNameDispatcher = struct &::+ (fun _ str -> StringSet.mem str pushback_modeled) <>$ capt_arg_payload $+...$--> StdVector.push_back ; +map_context_tenv (PatternMatch.Java.implements_lang "Integer") - &:: "" $ capt_arg_payload $+ capt_arg_payload $--> JavaInteger.constructor + &:: "" $ capt_arg_payload $+ capt_arg_payload $--> JavaInteger.init ; +map_context_tenv (PatternMatch.Java.implements_lang "Integer") &:: "equals" $ capt_arg_payload $+ capt_arg_payload $--> JavaInteger.equals ; +map_context_tenv (PatternMatch.Java.implements_lang "Integer")