[pulse] Fix printing order in contradiction for CItv and add tests

Summary:
- the order of call state was wrong when printing contradiction for CItv
- add a test for impurity

Reviewed By: jvillard

Differential Revision: D20646181

fbshipit-source-id: 1c86fd0a4

infer/src/pulse/PulseAbductiveDomain.ml

@@ -494,7 +494,7 @@ module PrePost = struct
           "caller addr %a%a but callee addr %a%a; %a=%a is unsatisfiable@\n\
            note: current call state was %a" AbstractValue.pp addr_caller (Pp.option CItv.pp)
           arith_caller AbstractValue.pp addr_callee (Pp.option CItv.pp) arith_callee
-          AbstractValue.pp addr_caller pp_call_state call_state AbstractValue.pp addr_callee
+          AbstractValue.pp addr_caller AbstractValue.pp addr_callee pp_call_state call_state
     | ArithmeticBo {addr_caller; addr_callee; arith_callee; call_state} ->
         F.fprintf fmt
           "callee addr %a%a is incompatible with caller addr %a's arithmetic constraints@\n\

infer/tests/codetoanalyze/java/impurity/TrickyExamples.java

@@ -0,0 +1,19 @@
+/*
+ * 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.
+ */
+class TrickyExamples {
+
+  int x;
+
+  // pulse summary only includes a single disjunct for everything upto the throw statement.
+  void loop_impure_FN() {
+    if (x > 10) {
+      throw new IllegalArgumentException("x too big");
+    }
+    x = 0;
+    for (int i = 0; i < 10; i++) {}
+  }
+}