From b7b7e89159910cf644226a76889a6883d9747489 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Mon, 10 May 2021 08:30:44 -0700 Subject: [PATCH] [pulse] Address some modeled fields as pointers Summary: This diff addresses `GenericArrayBackedCollection.field` and others as pointers. The modeled fields are used as non-pointer struct fields, but their actual semantics are pointers that may have side effects. For example, `GenericArrayBackedCollection.field` is used for keeping an information that the previous vector's address could be invalid. ``` void foo(vector v) { v.push_back(0); // v's previous address may be invalid after push_back // PRE: {v -> {backing_array -> v1}} // POST: {v -> {backing_array -> v2}} // ATTR: {v1 may be invalidated} } ``` However, if we revert the modeled field values, it will return incorrect summary as follows, by reverting non-pointer parameter values. ``` // PRE: {v -> {backing_array -> v1}} // POST: {v -> {backing_array -> v1}} // ATTR: {v1 may be invalidated} ``` Reviewed By: jvillard Differential Revision: D28324161 fbshipit-source-id: 96451d4b0 --- infer/src/pulse/PulseModels.ml | 18 +++++------ infer/src/pulse/PulseOperations.ml | 26 ++++++++++++++-- infer/src/pulse/PulseOperations.mli | 31 ++++++++++++++++++- .../codetoanalyze/cpp/impurity/issues.exp | 12 +++---- .../tests/codetoanalyze/cpp/pulse/vector.cpp | 10 ++++++ .../codetoanalyze/java/impurity/issues.exp | 22 ++++++------- 6 files changed, 90 insertions(+), 29 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 4bc0c2d33..72c63c827 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -674,7 +674,7 @@ module GenericArrayBackedCollection = struct let access = HilExp.Access.FieldAccess field let eval mode location collection astate = - PulseOperations.eval_access mode location collection access astate + PulseOperations.eval_deref_access mode location collection access astate let eval_element location internal_array index astate = @@ -690,14 +690,14 @@ module GenericArrayBackedCollection = struct let eval_pointer_to_last_element location collection astate = let+ astate, pointer = - PulseOperations.eval_access Write location collection (FieldAccess last_field) astate + PulseOperations.eval_deref_access Write location collection (FieldAccess last_field) astate in let astate = AddressAttributes.mark_as_end_of_collection (fst pointer) astate in (astate, pointer) let eval_is_empty location collection astate = - PulseOperations.eval_access Write location collection (FieldAccess is_empty) astate + PulseOperations.eval_deref_access Write location collection (FieldAccess is_empty) astate end module GenericArrayBackedCollectionIterator = struct @@ -747,7 +747,7 @@ module GenericArrayBackedCollectionIterator = struct GenericArrayBackedCollection.eval Read location init astate in let* astate = - PulseOperations.write_field location ~ref GenericArrayBackedCollection.field + PulseOperations.write_deref_field location ~ref GenericArrayBackedCollection.field ~obj:(arr_addr, event :: arr_hist) astate in @@ -872,9 +872,9 @@ module StdVector = struct GenericArrayBackedCollection.eval NoAccess location vector astate in PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate - >>= PulseOperations.invalidate_access location (StdVector vector_f) vector + >>= PulseOperations.invalidate_deref_access location (StdVector vector_f) vector GenericArrayBackedCollection.access - >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace + >>= PulseOperations.havoc_deref_field location vector GenericArrayBackedCollection.field trace let init_list_constructor this init_list : model = @@ -882,7 +882,7 @@ module StdVector = struct let event = ValueHistory.Call {f= Model "std::vector::vector()"; location; in_call= []} in let<*> astate, init_copy = PulseOperations.shallow_copy location init_list astate in let<+> astate = - PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field + PulseOperations.write_deref_field location ~ref:this GenericArrayBackedCollection.field ~obj:(fst init_copy, event :: snd init_copy) astate in @@ -922,7 +922,7 @@ module StdVector = struct in let<*> astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in let<+> astate = - PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field + PulseOperations.write_deref_field location ~ref:iter GenericArrayBackedCollection.field ~obj:(arr_addr, pointer_hist) astate >>= PulseOperations.write_field location ~ref:iter GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val @@ -941,7 +941,7 @@ module StdVector = struct let pointer_hist = event :: snd iter in let pointer_val = (pointer_addr, pointer_hist) in let<*> astate = - PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field + PulseOperations.write_deref_field location ~ref:iter GenericArrayBackedCollection.field ~obj:(arr_addr, pointer_hist) astate in let<+> astate = diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 0f54fe107..26ebf4446 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -179,6 +179,11 @@ let eval_access ?must_be_valid_reason mode location addr_hist access astate = Memory.eval_edge addr_hist access astate +let eval_deref_access ?must_be_valid_reason mode location addr_hist access astate = + let* astate, addr_hist = eval_access Read location addr_hist access astate in + eval_access ?must_be_valid_reason mode location addr_hist Dereference astate + + let eval_access_biad_isl mode location addr_hist access astate = let map_ok addr_hist access results = List.map results ~f:(fun result -> @@ -369,12 +374,19 @@ let write_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = write_access location addr_trace_ref (FieldAccess field) addr_trace_obj astate +let write_deref_field location ~ref:addr_trace_ref field ~obj:addr_trace_obj astate = + let* astate, addr_hist = eval_access Read location addr_trace_ref (FieldAccess field) astate in + write_deref location ~ref:addr_hist ~obj:addr_trace_obj astate + + let write_arr_index location ~ref:addr_trace_ref ~index ~obj:addr_trace_obj astate = write_access location addr_trace_ref (ArrayAccess (StdTyp.void, index)) addr_trace_obj astate -let havoc_field location addr_trace field trace_obj astate = - write_field location ~ref:addr_trace field ~obj:(AbstractValue.mk_fresh (), trace_obj) astate +let havoc_deref_field location addr_trace field trace_obj astate = + write_deref_field location ~ref:addr_trace field + ~obj:(AbstractValue.mk_fresh (), trace_obj) + astate let allocate procname location addr_trace astate = @@ -435,6 +447,16 @@ let invalidate_access location cause ref_addr_hist access astate = astate +let invalidate_deref_access location cause ref_addr_hist access astate = + let astate, addr_hist = Memory.eval_edge ref_addr_hist access astate in + let astate, (addr_obj, hist_obj) = Memory.eval_edge addr_hist Dereference astate in + invalidate + (MemoryAccess {pointer= ref_addr_hist; access; hist_obj_default= hist_obj}) + location cause + (addr_obj, snd ref_addr_hist) + astate + + let invalidate_array_elements location cause addr_trace astate = let+ astate = check_addr_access NoAccess location addr_trace astate in match Memory.find_opt (fst addr_trace) astate with diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index e8d6c3e5e..cfa0c878c 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -117,17 +117,28 @@ val eval_access : (** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if so dereferences it according to the access. *) +val eval_deref_access : + ?must_be_valid_reason:Invalidation.must_be_valid_reason + -> access_mode + -> Location.t + -> AbstractValue.t * ValueHistory.t + -> BaseMemory.Access.t + -> t + -> (t * (AbstractValue.t * ValueHistory.t)) AccessResult.t +(** Like [eval_access] but does additional dereference. *) + val eval_proc_name : Location.t -> Exp.t -> t -> (t * Procname.t option) AccessResult.t val havoc_id : Ident.t -> ValueHistory.t -> t -> t -val havoc_field : +val havoc_deref_field : Location.t -> AbstractValue.t * ValueHistory.t -> Fieldname.t -> ValueHistory.t -> t -> t AccessResult.t +(** Havoc dereferenced field address. *) val realloc_pvar : Tenv.t -> Pvar.t -> Typ.t -> Location.t -> t -> t @@ -142,6 +153,15 @@ val write_field : -> t AccessResult.t (** write the edge [ref --.field--> obj] *) +val write_deref_field : + Location.t + -> ref:AbstractValue.t * ValueHistory.t + -> Fieldname.t + -> obj:AbstractValue.t * ValueHistory.t + -> t + -> t AccessResult.t +(** write the edge [ref --.field--> _ --*--> obj] *) + val write_arr_index : Location.t -> ref:AbstractValue.t * ValueHistory.t @@ -207,6 +227,15 @@ val invalidate_access : -> t AccessResult.t (** record that what the address points via the access to is invalid *) +val invalidate_deref_access : + Location.t + -> Invalidation.t + -> AbstractValue.t * ValueHistory.t + -> BaseMemory.Access.t + -> t + -> t AccessResult.t +(** Like [invalidate_access] but invalidates dereferenced address. *) + val invalidate_array_elements : Location.t -> Invalidation.t -> AbstractValue.t * ValueHistory.t -> t -> t AccessResult.t (** record that all the array elements that address points to is invalid *) diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 301b2c8e6..c6f744cd0 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -28,9 +28,9 @@ codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FU codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter `x.*` modified here] codetoanalyze/cpp/impurity/unmodeled.cpp, output_stream_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function output_stream_impure,global variable `std::cout.*` modified here,call to skipped function std::basic_ostream>::operator<< occurs here,call to skipped function std::operator<<_> occurs here] codetoanalyze/cpp/impurity/unmodeled.cpp, random_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function random_impure,call to skipped function rand occurs here] -codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec.*` modified here] -codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter `vec.*` modified here] -codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec.*` modified here] -codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter `vec.*` modified here] -codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec.*` modified here] -codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers.*backing_array[]i` modified here] +codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec.*backing_array` modified here,parameter `vec.*` modified here] +codetoanalyze/cpp/impurity/vector.cpp, clear_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function clear_impure,parameter `vec.*backing_array` modified here,parameter `vec.*` modified here] +codetoanalyze/cpp/impurity/vector.cpp, insert_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function insert_impure,parameter `vec.*backing_array` modified here,parameter `vec.*` modified here] +codetoanalyze/cpp/impurity/vector.cpp, push_back_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_impure,parameter `vec.*backing_array` modified here,parameter `vec.*` modified here] +codetoanalyze/cpp/impurity/vector.cpp, push_back_in_loop_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function push_back_in_loop_impure,parameter `vec.*backing_array` modified here,parameter `vec.*` modified here] +codetoanalyze/cpp/impurity/vector.cpp, set_zero_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function set_zero_impure,parameter `numbers.*backing_array*[]i` modified here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index 3a9dee0a6..a91ccfd32 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -149,3 +149,13 @@ struct VectorA { f(x); } }; + +void push_back_wrapper() { + static std::vector v{}; + v.push_back(7); +} + +void call_push_back_wrapper_ok() { + push_back_wrapper(); + push_back_wrapper(); +} diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 5642a22e3..9df6c7be5 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -10,33 +10,33 @@ codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localit codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter `array.*[]*x` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter `array.*[]*bar` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_impure(int):int[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int[] Localities.get_impure(int),global variable `Localities.*pool*[]*[]` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.incrementAll_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list.*backing_array[]x` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list.*backing_array[]x` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list.*backing_array[]x` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list.*backing_array[]x` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.incrementAll_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.incrementAll_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list.*backing_array*[]x` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.makeAllZero_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.makeAllZero_impure(ArrayList),parameter `list.*backing_array*[]x` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.modify_first_el_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_first_el_impure(ArrayList),parameter `list.*backing_array*[]x` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.modify_via_call_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities.modify_via_call_impure(ArrayList),when calling `void Localities$Foo.inc_impure()` here,parameter `list.*backing_array*[]x` modified here] codetoanalyze/java/impurity/Localities.java, Localities.newHashCode_impure():int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.newHashCode_impure(),call to skipped function int Object.hashCode() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.add_impure(java.util.ArrayList):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.add_impure(ArrayList),parameter `list.**__infer_model_backing_collection_snd` modified here,parameter `list.**__infer_model_backing_collection_fst` modified here,parameter `list.**__infer_model_backing_collection_empty` modified here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.append_impure(java.lang.StringBuilder):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.append_impure(StringBuilder),parameter `strBuilder.*` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.append_impure(java.lang.StringBuilder):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.append_impure(StringBuilder),parameter `strBuilder.*backing_array` modified here,parameter `strBuilder.*` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_set_impure(ArrayList),when calling `void PurityModeled.list_set_impure(ArrayList)` here,parameter `list.**__infer_model_backing_collection_empty` modified here,when calling `void PurityModeled.list_set_impure(ArrayList)` here,parameter `list.*__infer_model_backing_collection_snd` modified here,when calling `void PurityModeled.list_set_impure(ArrayList)` here,parameter `list.*__infer_model_backing_collection_fst` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_impure(int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_timing_symb_unrelated_impure(int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_timing_symb_unrelated_impure(int,int),when calling `void PurityModeled.timing_call_in_loop_symb_impure(int)` here,call to skipped function long System.nanoTime() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.call_write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.call_write_impure(),when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.constant_loop_pure_FP():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.constant_loop_pure_FP() with empty pulse summary] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_add_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_add_impure(ArrayList),parameter `list.**__infer_model_backing_collection_snd` modified here,parameter `list.**__infer_model_backing_collection_fst` modified here,parameter `list.**__infer_model_backing_collection_empty` modified here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure(java.util.ArrayList,java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1.*` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_addall_impure(java.util.ArrayList,java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_addall_impure(ArrayList,ArrayList),parameter `list1.*backing_array` modified here,parameter `list1.*` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.list_set_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.list_set_impure(ArrayList),parameter `list.**__infer_model_backing_collection_empty` modified here,parameter `list.*__infer_model_backing_collection_snd` modified here,parameter `list.*__infer_model_backing_collection_fst` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_impure():double, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double PurityModeled.math_random_impure(),call to skipped function double Math.random() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.math_random_in_loop_impure(int):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int PurityModeled.math_random_in_loop_impure(int),when calling `void PurityModeled.call_write_impure()` here,when calling `void PurityModeled.write_impure()` here,call to skipped function void PrintStream.write(byte[],int,int) occurs here,call to skipped function double Math.random() occurs here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.nested_remove_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.nested_remove_impure(ArrayList),parameter `list.*backing_array[]backing_array` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.nested_remove_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.nested_remove_impure(ArrayList),parameter `list.*backing_array*[]backing_array*` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.next_impure(java.util.Iterator):java.lang.Integer, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Integer PurityModeled.next_impure(Iterator),parameter `it.*` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.process_queue_impure(java.util.ArrayList,java.util.Queue):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.process_queue_impure(ArrayList,Queue),parameter `queue.**__infer_model_backing_collection_snd` modified here,parameter `queue.**__infer_model_backing_collection_fst` modified here,parameter `queue.**__infer_model_backing_collection_empty` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_all_directly_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_all_directly_impure(ArrayList),parameter `list.**__infer_model_backing_collection_snd` modified here,parameter `list.**__infer_model_backing_collection_fst` modified here,parameter `list.**__infer_model_backing_collection_empty` modified here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_all_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_all_impure(ArrayList),parameter `list.*backing_array` modified here,call to skipped function void PrintStream.println(String) occurs here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_fresh_impure(java.util.ArrayList):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.remove_fresh_impure(ArrayList),parameter `list.*backing_array` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_all_impure(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_all_impure(ArrayList),parameter `list.*backing_array*` modified here,call to skipped function void PrintStream.println(String) occurs here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_fresh_impure(java.util.ArrayList):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.remove_fresh_impure(ArrayList),parameter `list.*backing_array*` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure(java.util.Iterator):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure(Iterator),parameter `i.*` modified here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure_mult(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure_mult(ArrayList),when calling `String PurityModeled.remove_fresh_impure(ArrayList)` here,parameter `list.*backing_array` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_impure_mult(java.util.ArrayList):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.remove_impure_mult(ArrayList),when calling `String PurityModeled.remove_fresh_impure(ArrayList)` here,parameter `list.*backing_array*` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.remove_iterator_impure(java.util.Iterator):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.remove_iterator_impure(Iterator),parameter `listIterator.*` modified here] -codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.replace_impure(java.lang.String):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.replace_impure(String),parameter `s.*` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.replace_impure(java.lang.String):java.lang.String, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function String PurityModeled.replace_impure(String),parameter `s.*backing_array` modified here,parameter `s.*` modified here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_impure() with empty pulse summary] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.timing_call_in_loop_symb_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.timing_call_in_loop_symb_impure(int),call to skipped function long System.nanoTime() occurs here] codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.write_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.write_impure(),call to skipped function void PrintStream.write(byte[],int,int) occurs here]