From 428c18e6191302c0bd898a1ff2c4794d615305a2 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Mon, 8 Jun 2020 02:41:26 -0700 Subject: [PATCH] [starvation] fix static field printing Summary: The Java frontend translates java field accesses on an object reference as field (`.`) followed by dereference (`*`) exactly like the arrow operator in C. However, when the field is static, it generates just a field access `.`. This is a bug. This diff mitigates its effects for printing locks in starvation. Reviewed By: skcho Differential Revision: D21882875 fbshipit-source-id: 79846d826 --- infer/src/concurrency/AbstractAddress.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/infer/src/concurrency/AbstractAddress.ml b/infer/src/concurrency/AbstractAddress.ml index 92cc7ee57..aa9a5ca42 100644 --- a/infer/src/concurrency/AbstractAddress.ml +++ b/infer/src/concurrency/AbstractAddress.ml @@ -60,14 +60,18 @@ let pp_with_base pp_base fmt (base, accesses) = | FieldAccess field_name :: Dereference :: rest, _ -> let op = match !Language.curr_language with Clang -> "->" | Java -> "." in F.fprintf fmt "%a%s%a" pp_rev_accesses rest op Fieldname.pp field_name - | FieldAccess field_name :: rest, Clang -> + | FieldAccess field_name :: rest, _ -> + (* Java is allowed here only because the frontend is broken and generates + [FieldAccess] without a [Dereference] for static fields *) F.fprintf fmt "%a.%a" pp_rev_accesses rest Fieldname.pp field_name | Dereference :: rest, Clang -> F.fprintf fmt "*(%a)" pp_rev_accesses rest | TakeAddress :: rest, Clang -> F.fprintf fmt "&(%a)" pp_rev_accesses rest | access :: rest, Java -> - L.internal_error "Asked to print %a in Java mode@" (HilExp.Access.pp (fun _ _ -> ())) access ; + L.internal_error "Asked to print %a in Java mode@\n" + (HilExp.Access.pp (fun _ _ -> ())) + access ; pp_rev_accesses fmt rest in pp_rev_accesses fmt (List.rev accesses)