From df49f318f6e4f5165a6768d7160623eac8552229 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 28 Nov 2019 06:32:02 -0800 Subject: [PATCH] [pulse] havoc formals passed by reference to unknown procedures Summary: This gets rid of false positives when something invalid (eg null) is passed by reference to an initialisation function. Havoc'ing what the contents of the pointer to results in being optimistic about said contents in the future. Also surprisingly gets rid of some FNs (which means it can also introduce FPs) in the `std::atomic` tests because a path condition becomes feasible with havoc'ing. There's a slight refinement possible where we don't havoc pointers to const but that's more involved and left as future work. Reviewed By: skcho Differential Revision: D18726203 fbshipit-source-id: 264b5daeb --- infer/src/pulse/Pulse.ml | 36 +++---------------- infer/src/pulse/PulseOperations.ml | 23 +++++++++--- infer/src/pulse/PulseOperations.mli | 10 ++++++ .../codetoanalyze/cpp/impurity/issues.exp | 4 ++- .../codetoanalyze/cpp/impurity/unmodeled.cpp | 2 +- .../codetoanalyze/cpp/impurity/vector.cpp | 3 +- .../tests/codetoanalyze/cpp/pulse/issues.exp | 6 +++- .../cpp/pulse/unknown_functions.cpp | 35 ++++++++++++++++++ .../java/impurity/Localities.java | 10 +++--- .../java/impurity/PurityModeled.java | 2 +- .../codetoanalyze/java/impurity/issues.exp | 5 +++ 11 files changed, 89 insertions(+), 47 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 405af0952..1f00e4e85 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -40,39 +40,13 @@ module PulseTransferFunctions = struct type extras = unit - let exec_unknown_call reason ret call actuals _flags call_loc astate = - let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in - let havoc_ret (ret, _) astate = PulseOperations.havoc_id ret [event] astate in - match proc_name_of_call call with - | Some callee_pname when Typ.Procname.is_constructor callee_pname -> ( - L.d_printfln "constructor call detected@." ; - match actuals with - | (object_ref, _) :: _ -> - PulseOperations.havoc_deref call_loc object_ref [event] astate >>| havoc_ret ret - | _ -> - Ok (havoc_ret ret astate) ) - | Some (Typ.Procname.ObjC_Cpp callee_pname) - when Typ.Procname.ObjC_Cpp.is_operator_equal callee_pname -> ( - L.d_printfln "operator= detected@." ; - match actuals with - (* copy assignment *) - | [(lhs, _); _rhs] -> - PulseOperations.havoc_deref call_loc lhs [event] astate >>| havoc_ret ret - | _ -> - Ok (havoc_ret ret astate) ) - | _ -> - L.d_printfln "skipping unknown procedure@." ; - Ok (havoc_ret ret astate) - - - let interprocedural_call caller_summary ret call_exp actuals flags call_loc astate = + let interprocedural_call caller_summary ret call_exp actuals call_loc astate = match proc_name_of_call call_exp with | Some callee_pname -> PulseOperations.call ~caller_summary call_loc callee_pname ~ret ~actuals astate | None -> - L.d_printfln "Indirect call %a@\n" Exp.pp call_exp ; - exec_unknown_call (SkippedUnknownCall call_exp) ret call_exp actuals flags call_loc astate - >>| List.return + L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; + Ok [PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals astate] (** has an object just gone out of scope? *) @@ -131,9 +105,7 @@ module PulseTransferFunctions = struct ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ)) func_args in - let r = - interprocedural_call summary ret call_exp only_actuals_evaled flags call_loc astate - in + let r = interprocedural_call summary ret call_exp only_actuals_evaled call_loc astate in PerfEvent.(log (fun logger -> log_end_event logger ())) ; r in diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 71ef788d1..118e56767 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -438,6 +438,24 @@ let remove_vars vars location astate = if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable astate' +let unknown_call call_loc reason ~ret ~actuals astate = + let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in + let havoc_ret (ret, _) astate = havoc_id ret [event] astate in + let havoc_actual_if_ptr (actual, typ) astate = + if Typ.is_pointer typ then + (* TODO: to avoid false negatives, we should not havoc when the corresponding formal is a + pointer to const *) + (* HACK: write through the pointer even if it is invalid. This is to avoid raising issues when + havoc'ing pointer parameters (which normally causes a [check_valid] call. *) + let fresh_value = AbstractValue.mk_fresh () in + Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate + else astate + in + L.d_printfln "skipping unknown procedure@." ; + List.fold actuals ~f:(fun astate actual_typ -> havoc_actual_if_ptr actual_typ astate) ~init:astate + |> havoc_ret ret + + let call ~caller_summary call_loc callee_pname ~ret ~actuals astate = match PulsePayload.read_full ~caller_summary ~callee_pname with | Some (callee_proc_desc, preposts) -> @@ -467,7 +485,4 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate = | None -> (* no spec found for some reason (unknown function, ...) *) L.d_printfln "No spec found for %a@\n" Typ.Procname.pp callee_pname ; - let event = - ValueHistory.Call {f= SkippedKnownCall callee_pname; location= call_loc; in_call= []} - in - Ok [havoc_id (fst ret) [event] astate] + Ok [unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals astate] diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 4c5e2441c..a5e0e9f35 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -115,3 +115,13 @@ val call : -> t list access_result (** perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists *) + +val unknown_call : + Location.t + -> CallEvent.t + -> ret:Ident.t * 'a + -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list + -> t + -> t +(** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and + the return value as appropriate *) diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 2da6795e6..453d898ea 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -23,8 +23,10 @@ codetoanalyze/cpp/impurity/invalid_test.cpp, swap_impure, 0, IMPURE_FUNCTION, no codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter `x` of create_cycle_impure,parameter `x` modified here] codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter `pp` of invalidate_local_impure,parameter `pp` modified here] codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter `x` of 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` accessed here,global variable `std::cout` modified here] codetoanalyze/cpp/impurity/vector.cpp, assign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function assign_impure,parameter `vec` of 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` of 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` of 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` of 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` of 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_other` of push_back_in_loop_impure,assigned,parameter `vec_other` modified here,parameter `vec` of 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` of set_zero_impure,assigned,parameter `numbers` modified here] diff --git a/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp b/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp index 3ab8dc7b6..c5004422b 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp +++ b/infer/tests/codetoanalyze/cpp/impurity/unmodeled.cpp @@ -6,6 +6,6 @@ */ #include -void output_stream_impure_FN() { std::cout << "Hello, world!" << std::endl; } +void output_stream_impure() { std::cout << "Hello, world!" << std::endl; } int random_impure_FN() { std::rand(); } diff --git a/infer/tests/codetoanalyze/cpp/impurity/vector.cpp b/infer/tests/codetoanalyze/cpp/impurity/vector.cpp index 4903f259c..96cd9480f 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/impurity/vector.cpp @@ -32,8 +32,7 @@ struct A { int i; }; -// iterators are not modeled in pulse yet -int set_zero_impure_FN(std::vector& numbers) { +int set_zero_impure(std::vector& numbers) { for (auto& num : numbers) { num.i = 0; } diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index 5ea42fa36..be82ee53a 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -1,4 +1,4 @@ -codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] +codetoanalyze/cpp/pulse/basic_string.cpp, use_range_of_invalidated_temporary_string_bad, 2, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `s` declared here,when calling `setLanguage` here,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,return from call to `Range::Range`,passed as argument to `std::basic_string::~basic_string()` (modelled),return from call to `std::basic_string::~basic_string()` (modelled),was invalidated by `delete`,use-after-lifetime part of the trace starts here,variable `s` declared here,passed as argument to `setLanguage`,variable `C++ temporary` declared here,passed as argument to `Range::Range`,parameter `str` of Range::Range,passed as argument to `std::basic_string::data()` (modelled),return from call to `std::basic_string::data()` (modelled),assigned,return from call to `Range::Range`,return from call to `setLanguage`,when calling `Range::operator[]` here,parameter `this` of Range::operator[],invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_branch_bad, 6, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_branch_bad,invalid access occurs here] codetoanalyze/cpp/pulse/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,was invalidated by `delete`,use-after-lifetime part of the trace starts here,parameter `ptr` of multiple_invalidations_loop_bad,invalid access occurs here] codetoanalyze/cpp/pulse/closures.cpp, call_lambda_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,assigned,when calling `call_lambda_bad::lambda_closures.cpp:163:12::operator()` here,parameter `s` of call_lambda_bad::lambda_closures.cpp:163:12::operator(),invalid access occurs here] @@ -37,6 +37,10 @@ codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_strong codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_strong_impossible_npe2_ok, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_weak_impossible_npe1_ok, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::FP_compare_exchange_weak_impossible_npe2_ok, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::compare_exchange_strong_possible_npe1_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::compare_exchange_strong_possible_npe2_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::compare_exchange_weak_possible_npe1_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::compare_exchange_weak_possible_npe2_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::exchange_possible_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::load_store_possible_npe_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::pre_increment_decrement_test_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp b/infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp new file mode 100644 index 000000000..ad8119cc2 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/pulse/unknown_functions.cpp @@ -0,0 +1,35 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +struct X { + ~X(){}; + void foo(); +}; + +void unknown_init_ptr_by_ref(X** x); +void unknown_no_init_ptr(X* const* x); // cannot init because const + +void init_ok() { + X* p = nullptr; + unknown_init_ptr_by_ref(&p); + p->foo(); +} + +void const_no_init_bad_FN() { + X* p = nullptr; + unknown_no_init_ptr(&p); + p->foo(); +} + +void unknown_init_value_by_ref(X* x); + +void wrap_unknown_init(X* x) { unknown_init_value_by_ref(x); } + +void call_unknown_init_interproc_ok() { + X* p = nullptr; + wrap_unknown_init(p); + p->foo(); +} diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java index 6c2d743e5..4aeea2947 100644 --- a/infer/tests/codetoanalyze/java/impurity/Localities.java +++ b/infer/tests/codetoanalyze/java/impurity/Localities.java @@ -9,7 +9,7 @@ import java.util.Iterator; class Localities { // @pure - boolean contains_pure(Integer i, ArrayList list) { + boolean contains_pure_FP(Integer i, ArrayList list) { Iterator listIterator = list.iterator(); while (listIterator.hasNext()) { Integer el = listIterator.next(); @@ -21,7 +21,7 @@ class Localities { } // @mod:{list} - void makeAllZero_impure_FN(ArrayList list) { + void makeAllZero_impure(ArrayList list) { Iterator listIterator = list.iterator(); while (listIterator.hasNext()) { Foo foo = listIterator.next(); @@ -30,7 +30,7 @@ class Localities { } // @mod:{list} - void incrementAll_impure_FN(ArrayList list) { + void incrementAll_impure(ArrayList list) { Iterator listIterator = list.iterator(); while (listIterator.hasNext()) { Foo foo = listIterator.next(); @@ -41,7 +41,7 @@ class Localities { // @pure void call_impure_with_fresh_args_pure() { ArrayList list = new ArrayList(); - makeAllZero_impure_FN(list); + makeAllZero_impure(list); } class Bar { @@ -74,7 +74,7 @@ class Localities { } // @pure, @loc:{} - int length_pure(ArrayList list) { + int length_pure_FP(ArrayList list) { Counter c = new Counter(); for (Integer i : list) { c.inc_impure(); diff --git a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java index f844127c9..facc8a335 100644 --- a/infer/tests/codetoanalyze/java/impurity/PurityModeled.java +++ b/infer/tests/codetoanalyze/java/impurity/PurityModeled.java @@ -10,7 +10,7 @@ class PurityModeled { return Math.random(); } - void arraycopy_pure(int[] src) { + void arraycopy_pure_FP(int[] src) { int[] dst = {5, 10, 20, 30, 40, 50}; // copies an array from the specified source array System.arraycopy(src, 0, dst, 0, 1); diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index de8630d48..a016ad5bf 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -5,12 +5,17 @@ codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_ codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` modified here] codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter `this` of void Localities$Counter.inc_impure(),parameter `this` modified here] codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter `this` of void Localities$Foo.inc_impure(),parameter `this` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.contains_pure_FP(java.lang.Integer,java.util.ArrayList):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `i` of boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `i` modified here,parameter `list` of boolean Localities.contains_pure_FP(Integer,ArrayList),parameter `list` modified here] codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter `a` of boolean Localities.copy_ref_impure(int[],int),assigned,parameter `a` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here] 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` of Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` 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` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here,parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` 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),parameter `list` of void Localities.incrementAll_impure(ArrayList),parameter `list` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.length_pure_FP(java.util.ArrayList):int, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function int Localities.length_pure_FP(ArrayList),parameter `list` of int Localities.length_pure_FP(ArrayList),parameter `list` 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` of void Localities.makeAllZero_impure(ArrayList),parameter `list` 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` of void Localities.modify_first_el_impure(ArrayList),passed as argument to `Collection.get()` (modelled),return from call to `Collection.get()` (modelled),assigned,assigned,parameter `list` 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),parameter `list` of void Localities.modify_via_call_impure(ArrayList),passed as argument to `Localities$Foo Localities.get_first_pure(ArrayList)`,return from call to `Localities$Foo Localities.get_first_pure(ArrayList)`,assigned,when calling `void Localities$Foo.inc_impure()` here,parameter `this` of void Localities$Foo.inc_impure(),parameter `list` modified here] +codetoanalyze/java/impurity/PurityModeled.java, PurityModeled.arraycopy_pure_FP(int[]):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` of void PurityModeled.arraycopy_pure_FP(int[]),parameter `src` modified here] codetoanalyze/java/impurity/Test.java, Test.Test(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.Test(int),global variable `Test` accessed here,global variable `Test` modified here] codetoanalyze/java/impurity/Test.java, Test.alias_impure(int[],int,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.alias_impure(int[],int,int),parameter `array` of void Test.alias_impure(int[],int,int),assigned,parameter `array` modified here] codetoanalyze/java/impurity/Test.java, Test.call_impure_impure(int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Test.call_impure_impure(int),parameter `this` of void Test.call_impure_impure(int),when calling `void Test.set_impure(int,int)` here,parameter `this` of void Test.set_impure(int,int),parameter `this` modified here]