From da0933fd7998e291ef7d18c6e3bdbdf38d30126d Mon Sep 17 00:00:00 2001 From: Peter O'Hearn Date: Wed, 15 Jun 2016 15:03:59 -0700 Subject: [PATCH] first try at dereferencing lock on monitor enter Reviewed By: sblackshear Differential Revision: D3430360 fbshipit-source-id: 89f0018 --- infer/src/java/jTrans.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 73934f6f7..ffa42d1dd 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -796,8 +796,12 @@ let rec instruction context pc instr : translation = let instrs, sil_expr, sil_type = expression context pc expr in let builtin_const = Sil.Const (Sil.Cfun builtin) in let instr = Sil.Call ([], builtin_const, [(sil_expr, sil_type)], loc, Sil.cf_default) in + let typ_no_ptr = match sil_type with + | Typ.Tptr (typ, _) -> typ + | _ -> sil_type in + let deref_instr = create_sil_deref sil_expr typ_no_ptr loc in let node_kind = Cfg.Node.Stmt_node node_desc in - Instr (create_node node_kind (instrs @ [instr])) in + Instr (create_node node_kind (instrs @ [deref_instr; instr] )) in try match instr with | JBir.AffectVar (var, expr) ->