From ab7d569e5003a8ee1004e4aa4ede7b0c960b15a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 20 May 2021 02:37:07 -0700 Subject: [PATCH] [refactor] Remove redundant calls Reviewed By: jvillard Differential Revision: D28540798 fbshipit-source-id: 5d86649e5 --- infer/src/pulse/PulseModels.ml | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) 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()"