diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 0d581d2be..4311c998c 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -1077,8 +1077,6 @@ module JavaCollection = struct astate |> ok_continue - 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 *) let* astate, coll_val = PulseOperations.eval_access Read location coll Dereference astate in @@ -1101,7 +1099,7 @@ 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 {location; ret= ret_id, _} astate -> 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 @@ -1618,8 +1616,8 @@ module ProcNameDispatcher = struct &:: "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 ~desc:"Collection.add()" + &:: "add" <>$ capt_arg_payload $+ any_arg $+ capt_arg_payload + $--> JavaCollection.add ~desc:"Collection.add()" ; +map_context_tenv PatternMatch.Java.implements_collection &:: "remove" &++> JavaCollection.remove ~desc:"Collection.remove" @@ -1682,8 +1680,6 @@ module ProcNameDispatcher = struct ; +map_context_tenv PatternMatch.Java.implements_iterator &:: "remove" <>$ capt_arg_payload $+...$--> JavaIterator.remove ~desc:"remove" - ; +map_context_tenv PatternMatch.Java.implements_map - &:: "put" <>$ capt_arg_payload $+...$--> StdVector.push_back ; +map_context_tenv PatternMatch.Java.implements_map &:: "putAll" <>$ capt_arg_payload $+...$--> StdVector.push_back ; -"std" &:: "vector" &:: "reserve" <>$ capt_arg_payload $+...$--> StdVector.reserve @@ -1691,8 +1687,7 @@ module ProcNameDispatcher = struct &:: "get" <>$ capt_arg_payload $+ capt_arg_payload $--> StdVector.at ~desc:"Collection.get()" ; +map_context_tenv PatternMatch.Java.implements_list - &:: "set" <>$ capt_arg_payload $+ capt_arg_payload $+ capt_arg_payload - $--> JavaCollection.set + &:: "set" <>$ capt_arg_payload $+ any_arg $+ capt_arg_payload $--> JavaCollection.set ; +map_context_tenv PatternMatch.Java.implements_iterator &:: "hasNext" &--> Misc.nondet ~fn_name:"Iterator.hasNext()"