From f7baf845fd2d1e6ce1eda7fbb74030e2e3d4c916 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 25 Mar 2020 08:41:38 -0700 Subject: [PATCH] [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 | 2 +- .../java/impurity/TrickyExamples.java | 19 +++++++++++++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/java/impurity/TrickyExamples.java diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 073ffdb56..96ad0602e 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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\ diff --git a/infer/tests/codetoanalyze/java/impurity/TrickyExamples.java b/infer/tests/codetoanalyze/java/impurity/TrickyExamples.java new file mode 100644 index 000000000..bfc6bcd90 --- /dev/null +++ b/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++) {} + } +}