[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

@@ -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 =

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 =
+let havoc_deref_field location addr_trace field trace_obj astate =
-  write_field location ~ref:addr_trace field ~obj:(AbstractValue.mk_fresh (), 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

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 *)

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<char,std::char_traits<char>>::operator<< occurs here,call to skipped function std::operator<<<std::char_traits<char>_> 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, 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.*` 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.*` 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.*` 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.*` 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]
+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]

infer/tests/codetoanalyze/cpp/pulse/vector.cpp

@@ -149,3 +149,13 @@ struct VectorA {
     f(x);
   }
 };
+
+void push_back_wrapper() {
+  static std::vector<int> v{};
+  v.push_back(7);
+}
+
+void call_push_back_wrapper_ok() {
+  push_back_wrapper();
+  push_back_wrapper();
+}

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.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.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_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.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_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_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]