[infer][java] the skip-implementation option should preserve the line number information, which is not the case when translated those methods as native methods

Summary: This should be equivalent as far as bug finding is concerned, but will allow the analysis traces to jump into the skipped methods.

Reviewed By: sblackshear

Differential Revision: D5778245

fbshipit-source-id: 3fd061f

infer/src/java/jFrontend.ml

@@ -88,7 +88,10 @@ let add_edges (context: JContext.t) start_node exn_node exit_nodes method_body_n
 (** Add a concrete method. *)
 let add_cmethod source_file program linereader icfg cm proc_name =
   let cn, _ = JBasics.cms_split cm.Javalib.cm_class_method_signature in
-  match JTrans.create_cm_procdesc source_file program linereader icfg cm proc_name with
+  let skip_implementation = Inferconfig.skip_implementation_matcher source_file proc_name in
+  match
+    JTrans.create_cm_procdesc source_file program linereader icfg cm proc_name skip_implementation
+  with
   | None
    -> ()
   | Some (procdesc, _, jbir_code)
@@ -101,7 +104,7 @@ let add_cmethod source_file program linereader icfg cm proc_name =
         | None
          -> L.(die InternalError) "No exn node found for %s" (Typ.Procname.to_string proc_name)
       in
-      let instrs = JBir.code jbir_code in
+      let instrs = if skip_implementation then Array.of_list [] else JBir.code jbir_code in
       let context = JContext.create_context icfg procdesc jbir_code cn source_file program in
       let method_body_nodes = Array.mapi ~f:(JTrans.instruction context) instrs in
       add_edges context start_node exn_node [exit_node] method_body_nodes jbir_code false
@@ -157,9 +160,6 @@ let create_icfg source_file linereader program icfg cn node =
          -> ignore (JTrans.create_am_procdesc source_file program icfg am proc_name)
         | Javalib.ConcreteMethod cm when JTrans.is_java_native cm
          -> ignore (JTrans.create_native_procdesc source_file program icfg cm proc_name)
-        | Javalib.ConcreteMethod cm
-          when Inferconfig.skip_implementation_matcher source_file proc_name
-         -> ignore (JTrans.create_native_procdesc source_file program icfg cm proc_name)
         | Javalib.ConcreteMethod cm
          -> add_cmethod source_file program linereader icfg cm proc_name ) ;
         Cg.add_defined_node icfg.JContext.cg proc_name

infer/src/java/jTrans.ml

@@ -335,7 +335,7 @@ let create_native_procdesc source_file program icfg cm proc_name =
   create_empty_cfg proc_name source_file procdesc
 
 (** Creates a procedure description. *)
-let create_cm_procdesc source_file program linereader icfg cm proc_name =
+let create_cm_procdesc source_file program linereader icfg cm proc_name skip_implementation =
   let cfg = icfg.JContext.cfg in
   let tenv = icfg.JContext.tenv in
   let m = Javalib.ConcreteMethod cm in
@@ -359,7 +359,7 @@ let create_cm_procdesc source_file program linereader icfg cm proc_name =
         ; exceptions= List.map ~f:JBasics.cn_name cm.Javalib.cm_exceptions
         ; formals
         ; is_bridge_method= cm.Javalib.cm_bridge
-        ; is_defined= true
+        ; is_defined= not skip_implementation
         ; is_model= Config.models_mode
         ; is_synthetic_method= cm.Javalib.cm_synthetic
         ; is_java_synchronized_method= cm.Javalib.cm_synchronized

infer/src/java/jTrans.mli

@@ -33,7 +33,7 @@ val create_native_procdesc :
 
 val create_cm_procdesc :
   SourceFile.t -> JClasspath.program -> Printer.LineReader.t -> JContext.icfg
-  -> JCode.jcode Javalib.concrete_method -> Typ.Procname.t
+  -> JCode.jcode Javalib.concrete_method -> Typ.Procname.t -> bool
   -> (Procdesc.t * Javalib_pack.JCode.jcode * JBir.t) option
 (** [create_procdesc source_file program linereader icfg cm proc_name] creates
     a procedure description for the concrete method cm and adds it to cfg *)