From d41d452b673a5f0e6549b0b6897eaafd8ec4fed5 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Sat, 26 Mar 2016 04:17:18 -0700 Subject: [PATCH] Make eradicate work in the absence of procdescs for callees. Summary:public Eradicate need the procedure attributes for callees. It relies on the java front-end to create proc descs for callees that are declared but not defined. This diff remove that needs, and when a callee without prodedure attributes is found, it creates one on the fly. The attribute created is similar to what the Java front-end would do, except that the number and types of arguments are part of the call instruction, so they can be used to create the formal parameters. Reviewed By: jeremydubreil Differential Revision: D3073904 fb-gh-sync-id: 381ff67 fbshipit-source-id: 381ff67 --- infer/lib/python/inferlib/jwlib.py | 4 -- infer/src/backend/iList.ml | 9 ++++ infer/src/backend/iList.mli | 3 ++ infer/src/backend/interproc.ml | 2 +- infer/src/backend/symExec.mli | 3 ++ infer/src/checkers/checkDeadCode.ml | 6 +-- infer/src/checkers/checkTraceCallSequence.ml | 6 +-- infer/src/checkers/constantPropagation.ml | 10 ++-- infer/src/checkers/constantPropagation.mli | 2 +- infer/src/checkers/dataflow.ml | 14 +++--- infer/src/checkers/dataflow.mli | 4 +- infer/src/checkers/repeatedCallsChecker.ml | 10 ++-- infer/src/checkers/sqlChecker.ml | 4 +- infer/src/eradicate/eradicate.ml | 12 ++--- infer/src/eradicate/typeCheck.ml | 49 ++++++++++++++++---- infer/src/eradicate/typeCheck.mli | 2 +- infer/src/eradicate/typeState.ml | 3 +- infer/src/eradicate/typeState.mli | 3 +- infer/src/java/jConfig.ml | 4 -- infer/src/java/jTrans.ml | 3 -- 20 files changed, 94 insertions(+), 59 deletions(-) diff --git a/infer/lib/python/inferlib/jwlib.py b/infer/lib/python/inferlib/jwlib.py index d4ad6db32..bb9333687 100644 --- a/infer/lib/python/inferlib/jwlib.py +++ b/infer/lib/python/inferlib/jwlib.py @@ -257,10 +257,6 @@ class AnalyzerWithFrontendWrapper(analyze.AnalyzerWrapper): if self.args.android_harness: infer_cmd.append('-harness') - if self.args.android_harness or \ - self.args.analyzer in [config.ANALYZER_ERADICATE, - config.ANALYZER_CAPTURE]: - os.environ['INFER_CREATE_CALLEE_PDESC'] = 'Y' return analyze.run_command( infer_cmd, diff --git a/infer/src/backend/iList.ml b/infer/src/backend/iList.ml index fa60fa05e..9a73db16a 100644 --- a/infer/src/backend/iList.ml +++ b/infer/src/backend/iList.ml @@ -100,6 +100,15 @@ let append l1 l2 = let map f l = rev (rev_map f l) +(** tail-recursive variant of List.mapi *) +let mapi f l = + let i = ref 0 in + rev (rev_map + (fun x -> + incr i; + f (!i - 1) x) + l) + (** Remove consecutive equal elements from a list (according to the given comparison functions) *) let remove_duplicates compare l = let rec remove compare acc = function diff --git a/infer/src/backend/iList.mli b/infer/src/backend/iList.mli index ac708dc57..6d7a240c1 100644 --- a/infer/src/backend/iList.mli +++ b/infer/src/backend/iList.mli @@ -45,6 +45,9 @@ val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b (** tail-recursive variant of List.map *) val map : ('a -> 'b) -> 'a list -> 'b list +(** tail-recursive variant of List.mapi *) +val mapi : (int -> 'a -> 'b) -> 'a list -> 'b list + (** Like List.mem but without builtin equality *) val mem : ('a -> 'b -> bool) -> 'a -> 'b list -> bool diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 2505c2ff7..77cc7ff32 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -478,7 +478,7 @@ let do_symbolic_execution handle_exn tenv let pdesc = Cfg.Node.get_proc_desc node in State.mark_execution_start node; (* build the const map lazily *) - State.set_const_map (ConstantPropagation.build_const_map pdesc); + State.set_const_map (ConstantPropagation.build_const_map tenv pdesc); check_assignement_guard node; let instrs = Cfg.Node.get_instrs node in (* fresh normal vars must be fresh w.r.t. instructions *) diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli index c18d44242..af3da4493 100644 --- a/infer/src/backend/symExec.mli +++ b/infer/src/backend/symExec.mli @@ -10,6 +10,9 @@ (** Symbolic Execution *) +(** Lookup Java types by name. *) +val lookup_java_typ_from_string : Sil.tenv -> string -> Sil.typ + (** print the builtin functions and exit *) val print_builtins : unit -> unit diff --git a/infer/src/checkers/checkDeadCode.ml b/infer/src/checkers/checkDeadCode.ml index 90ce6dd3b..b8153453a 100644 --- a/infer/src/checkers/checkDeadCode.ml +++ b/infer/src/checkers/checkDeadCode.ml @@ -50,7 +50,7 @@ module State = struct Cfg.NodeSet.cardinal t.visited end -let do_node node (s : State.t) : (State.t list) * (State.t list) = +let do_node _ node (s : State.t) : (State.t list) * (State.t list) = let s' = State.add_visited node s in if verbose then L.stderr " N:%a (#visited: %a)@." Cfg.Node.pp node @@ -87,7 +87,7 @@ let check_final_state proc_name proc_desc final_s = end (** Simple check for dead code. *) -let callback_check_dead_code { Callbacks.proc_desc; proc_name } = +let callback_check_dead_code { Callbacks.proc_desc; proc_name; tenv } = let module DFDead = MakeDF(struct type t = State.t @@ -100,7 +100,7 @@ let callback_check_dead_code { Callbacks.proc_desc; proc_name } = let do_check () = begin if verbose then L.stderr "@.--@.PROC: %a@." Procname.pp proc_name; - let transitions = DFDead.run proc_desc State.initial in + let transitions = DFDead.run tenv proc_desc State.initial in let exit_node = Cfg.Procdesc.get_exit_node proc_desc in match transitions exit_node with | DFDead.Transition (pre_final_s, _, _) -> diff --git a/infer/src/checkers/checkTraceCallSequence.ml b/infer/src/checkers/checkTraceCallSequence.ml index f7039d78a..e89691e3d 100644 --- a/infer/src/checkers/checkTraceCallSequence.ml +++ b/infer/src/checkers/checkTraceCallSequence.ml @@ -300,7 +300,7 @@ end (** State transformation for a cfg node. *) -let do_node pn pd idenv node (s : State.t) : (State.t list) * (State.t list) = +let do_node pn pd idenv _ node (s : State.t) : (State.t list) * (State.t list) = if verbose then L.stderr "N:%d S:%s@." (Cfg.Node.get_id node) (State.to_string s); let curr_state = ref s in @@ -321,7 +321,7 @@ let check_final_state proc_name proc_desc exit_node final_s = (** Check that the trace calls are balanced. This is done by using the most general control flow including exceptions. The begin() and end() function are assumed not to throw exceptions. *) -let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv } : unit = +let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv; tenv } : unit = let module DFTrace = MakeDF(struct type t = State.t @@ -337,7 +337,7 @@ let callback_check_trace_call_sequence { Callbacks.proc_desc; proc_name; idenv } let do_check () = begin if verbose then L.stderr "@.--@.PROC: %a@." Procname.pp proc_name; - let transitions = DFTrace.run proc_desc State.balanced in + let transitions = DFTrace.run tenv proc_desc State.balanced in let exit_node = Cfg.Procdesc.get_exit_node proc_desc in match transitions exit_node with | DFTrace.Transition (final_s, _, _) -> diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml index 4e0cc13d0..58f800be3 100644 --- a/infer/src/checkers/constantPropagation.ml +++ b/infer/src/checkers/constantPropagation.ml @@ -45,7 +45,7 @@ module ConstantFlow = Dataflow.MakeDF(struct let proc_throws _ = Dataflow.DontKnow - let do_node node constants = + let do_node _ node constants = let do_instr constants instr = try @@ -125,8 +125,8 @@ module ConstantFlow = Dataflow.MakeDF(struct [constants], [constants] end) -let run proc_desc = - let transitions = ConstantFlow.run proc_desc ConstantMap.empty in +let run tenv proc_desc = + let transitions = ConstantFlow.run tenv proc_desc ConstantMap.empty in let get_constants node = match transitions node with | ConstantFlow.Transition (_, post_states, _) -> ConstantFlow.join post_states ConstantMap.empty @@ -136,8 +136,8 @@ let run proc_desc = type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option (** Build a const map lazily. *) -let build_const_map pdesc = - let const_map = lazy (run pdesc) in +let build_const_map tenv pdesc = + let const_map = lazy (run tenv pdesc) in let f node exp = try let map = (Lazy.force const_map) node in diff --git a/infer/src/checkers/constantPropagation.mli b/infer/src/checkers/constantPropagation.mli index e04681aff..9b8e6aac2 100644 --- a/infer/src/checkers/constantPropagation.mli +++ b/infer/src/checkers/constantPropagation.mli @@ -10,4 +10,4 @@ type const_map = Cfg.Node.t -> Sil.exp -> Sil.const option (** Build a const map lazily. *) -val build_const_map : Cfg.Procdesc.t -> const_map +val build_const_map : Sil.tenv -> Cfg.Procdesc.t -> const_map diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 310569349..9db6c7610 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -21,7 +21,7 @@ module type DFStateType = sig val join : t -> t -> t (** Join two states (the old one is the first parameter). *) (** Perform a state transition on a node. *) - val do_node : Cfg.Node.t -> t -> (t list) * (t list) + val do_node : Sil.tenv -> Cfg.Node.t -> t -> (t list) * (t list) val proc_throws : Procname.t -> throws (** Can proc throw an exception? *) end @@ -35,7 +35,7 @@ module type DF = sig | Transition of state * state list * state list val join : state list -> state -> state - val run : Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) + val run : Sil.tenv -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) end (** Determine if the node can throw an exception. *) @@ -126,7 +126,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct H.replace t.exn_states node states_exn (** Run the worklist-based dataflow algorithm. *) - let run proc_desc state = + let run tenv proc_desc state = let t = let start_node = Cfg.Procdesc.get_start_node proc_desc in @@ -148,7 +148,7 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct t.worklist <- S.remove node t.worklist; try let state = H.find t.pre_states node in - let states_succ, states_exn = St.do_node node state in + let states_succ, states_exn = St.do_node tenv node state in propagate t node states_succ states_exn (node_throws node St.proc_throws) with Not_found -> () done in @@ -164,18 +164,18 @@ module MakeDF(St: DFStateType) : DF with type state = St.t = struct end (* MakeDF *) (** Example dataflow callback: compute the the distance from a node to the start node. *) -let callback_test_dataflow { Callbacks.proc_desc } = +let callback_test_dataflow { Callbacks.proc_desc; tenv } = let verbose = false in let module DFCount = MakeDF(struct type t = int let equal = int_equal let join n m = if n = 0 then m else n - let do_node n s = + let do_node _ n s = if verbose then L.stdout "visiting node %a with state %d@." Cfg.Node.pp n s; [s + 1], [s + 1] let proc_throws _ = DoesNotThrow end) in - let transitions = DFCount.run proc_desc 0 in + let transitions = DFCount.run tenv proc_desc 0 in let do_node node = match transitions node with | DFCount.Transition _ -> () diff --git a/infer/src/checkers/dataflow.mli b/infer/src/checkers/dataflow.mli index b5b0f1e0d..0fe947cd5 100644 --- a/infer/src/checkers/dataflow.mli +++ b/infer/src/checkers/dataflow.mli @@ -19,7 +19,7 @@ module type DFStateType = sig val join : t -> t -> t (** Join two states (the old one is the first parameter). *) (** Perform a state transition on a node. *) - val do_node : Cfg.Node.t -> t -> (t list) * (t list) + val do_node : Sil.tenv -> Cfg.Node.t -> t -> (t list) * (t list) val proc_throws : Procname.t -> throws (** Can proc throw an exception? *) end @@ -34,7 +34,7 @@ module type DF = sig val join : state list -> state -> state (** Run the dataflow analysis on a procedure starting from the given state. Returns a function to lookup the results of the analysis on every node *) - val run : Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) + val run : Sil.tenv -> Cfg.Procdesc.t -> state -> (Cfg.Node.t -> transition) end (** Functor to create an instance of a dataflow analysis. *) diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index 5498ca1b5..ae5d1d704 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -62,7 +62,7 @@ struct (** Check if the procedure performs an allocation operation. If [paths] is AllPaths, check if an allocation happens on all paths. If [paths] is SomePath, check if a path with an allocation exists. *) - let proc_performs_allocation pdesc paths : Location.t option = + let proc_performs_allocation tenv pdesc paths : Location.t option = let node_allocates node : Location.t option = let found = ref None in @@ -90,7 +90,7 @@ struct | Some loc1, Some _ -> Some loc1 (* left priority *) let join = _join paths - let do_node node lo1 = + let do_node _ node lo1 = let lo2 = node_allocates node in let lo' = (* use left priority join to implement transfer function *) _join SomePath lo1 lo2 in @@ -98,13 +98,13 @@ struct let proc_throws _ = Dataflow.DontKnow end) in - let transitions = DFAllocCheck.run pdesc None in + let transitions = DFAllocCheck.run tenv pdesc None in match transitions (Cfg.Procdesc.get_exit_node pdesc) with | DFAllocCheck.Transition (loc, _, _) -> loc | DFAllocCheck.Dead_state -> None (** Check repeated calls to the same procedure. *) - let check_instr get_proc_desc curr_pname curr_pdesc extension instr normalized_etl = + let check_instr tenv get_proc_desc curr_pname curr_pdesc extension instr normalized_etl = (** Arguments are not temporary variables. *) let arguments_not_temp args = @@ -128,7 +128,7 @@ struct match get_old_call instr_normalized_args extension with | Some (Sil.Call (_, _, _, loc_old, _)) -> begin - match proc_performs_allocation proc_desc AllPaths with + match proc_performs_allocation tenv proc_desc AllPaths with | Some alloc_loc -> let description = Printf.sprintf "call to %s seen before on line %d (may allocate at %s:%n)" diff --git a/infer/src/checkers/sqlChecker.ml b/infer/src/checkers/sqlChecker.ml index c50188af9..03d4d1bbf 100644 --- a/infer/src/checkers/sqlChecker.ml +++ b/infer/src/checkers/sqlChecker.ml @@ -11,7 +11,7 @@ module L = Logging (** Find SQL statements in string concatenations *) -let callback_sql { Callbacks.proc_desc; proc_name } = +let callback_sql { Callbacks.proc_desc; proc_name; tenv } = let verbose = false in (* Case insensitive SQL statement patterns *) @@ -62,7 +62,7 @@ let callback_sql { Callbacks.proc_desc; proc_name } = | _ -> () in try - let const_map = ConstantPropagation.build_const_map proc_desc in + let const_map = ConstantPropagation.build_const_map tenv proc_desc in if verbose then L.stdout "Analyzing %a...\n@." Procname.pp proc_name; Cfg.Procdesc.iter_instrs (do_instr const_map) proc_desc with _ -> () diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 1d43ddcd7..650ff5093 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -69,7 +69,7 @@ struct | None -> () let callback1 - find_canonical_duplicate calls_this checks get_proc_desc idenv curr_pname + tenv find_canonical_duplicate calls_this checks get_proc_desc idenv curr_pname curr_pdesc annotated_signature linereader proc_loc : bool * Extension.extension TypeState.t option = let mk_pvar s = Sil.mk_pvar s curr_pname in @@ -117,11 +117,11 @@ struct type t = Extension.extension TypeState.t let equal = TypeState.equal let join = TypeState.join Extension.ext - let do_node node typestate = + let do_node tenv node typestate = State.set_node node; let typestates_succ, typestates_exn = TypeCheck.typecheck_node - Extension.ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc + tenv Extension.ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc find_canonical_duplicate annotated_signature typestate node linereader in if trace then IList.iter (fun typestate_succ -> @@ -135,7 +135,7 @@ struct end) in let initial_typestate = get_initial_typestate () in do_before_dataflow initial_typestate; - let transitions = DFTypeCheck.run curr_pdesc initial_typestate in + let transitions = DFTypeCheck.run tenv curr_pdesc initial_typestate in match transitions (Cfg.Procdesc.get_exit_node curr_pdesc) with | DFTypeCheck.Transition (final_typestate, _, _) -> do_after_dataflow find_canonical_duplicate final_typestate; @@ -180,7 +180,7 @@ struct check_ret_type = []; }, ref false in callback1 - find_canonical_duplicate calls_this' checks' get_proc_desc idenv_pn + tenv find_canonical_duplicate calls_this' checks' get_proc_desc idenv_pn pname pdesc ann_sig linereader loc in let module Initializers = struct @@ -375,7 +375,7 @@ struct type extension = unit let ext = let empty = () in - let check_instr _ _ _ ext _ _ = ext in + let check_instr _ _ _ _ ext _ _ = ext in let join () () = () in let pp _ () = () in { diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 834778699..c9eaa6b8f 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -236,7 +236,8 @@ let rec typecheck_expr | _ -> tr_default (** Typecheck an instruction. *) -let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc curr_pname +let typecheck_instr + tenv ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc curr_pname curr_pdesc find_canonical_duplicate annotated_signature instr_ref linereader typestate instr = (* let print_current_state () = *) (* L.stdout "Current Typestate in node %a@\n%a@." *) @@ -558,15 +559,42 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc typestate | Sil.Call (_, Sil.Const (Sil.Cfun pn), _, _, _) when SymExec.function_is_builtin pn -> typestate (* skip othe builtins *) - | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), _etl, loc, cflags) - when Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname <> None -> + | Sil.Call + (ret_ids, + Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)), + etl_, + loc, + cflags) + -> Ondemand.analyze_proc_name ~propagate_exceptions:true curr_pdesc callee_pname; let callee_attributes = match Specs.proc_resolve_attributes (* AttributesTable.load_attributes *) callee_pname with - | Some proc_attributes -> proc_attributes - | None -> assert false in - - let etl = drop_unchecked_params calls_this callee_attributes _etl in + | Some proc_attributes -> + proc_attributes + | None -> + let formals = + IList.mapi + (fun i (_, typ) -> + let arg = + if i = 0 && + not (Procname.java_is_static callee_pname) + then "this" + else Printf.sprintf "arg%d" i in + (Mangled.from_string arg, typ)) + etl_ in + let ret_typ_str = Procname.java_get_return_type callee_pname_java in + let ret_type = + match SymExec.lookup_java_typ_from_string tenv ret_typ_str with + | Sil.Tstruct _ as typ -> Sil.Tptr (typ, Sil.Pk_pointer) + | typ -> typ in + let proc_attributes = + { (ProcAttributes.default callee_pname Config.Java) with + ProcAttributes.formals; + ret_type; + } in + proc_attributes in + + let etl = drop_unchecked_params calls_this callee_attributes etl_ in let call_params, typestate1 = let handle_et (e1, t1) (etl1, typestate1) = typecheck_expr_for_errors typestate e1 loc; @@ -798,7 +826,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc let extension = TypeState.get_extension typestate1 in let extension' = ext.TypeState.check_instr - get_proc_desc curr_pname curr_pdesc extension instr etl' in + tenv get_proc_desc curr_pname curr_pdesc extension instr etl' in TypeState.set_extension typestate1 extension' else typestate1 in let has_method pn name = match pn with @@ -1043,7 +1071,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc (** Typecheck the instructions in a cfg node. *) let typecheck_node - ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc + tenv ext calls_this checks idenv get_proc_desc curr_pname curr_pdesc find_canonical_duplicate annotated_signature typestate node linereader = let instrs = Cfg.Node.get_instrs node in @@ -1074,7 +1102,8 @@ let typecheck_node let instr_ref = (* keep unique instruction reference per-node *) TypeErr.InstrRef.gen instr_ref_gen in let instr' = - typecheck_instr ext calls_this checks node idenv get_proc_desc curr_pname curr_pdesc + typecheck_instr + tenv ext calls_this checks node idenv get_proc_desc curr_pname curr_pdesc find_canonical_duplicate annotated_signature instr_ref linereader typestate instr in handle_exceptions typestate instr; instr' in diff --git a/infer/src/eradicate/typeCheck.mli b/infer/src/eradicate/typeCheck.mli index 5c632e5c5..d27cea4b4 100644 --- a/infer/src/eradicate/typeCheck.mli +++ b/infer/src/eradicate/typeCheck.mli @@ -25,7 +25,7 @@ type checks = } val typecheck_node : - 'a TypeState.ext -> + Sil.tenv -> 'a TypeState.ext -> bool ref -> checks -> Idenv.t -> get_proc_desc -> Procname.t -> Cfg.Procdesc.t -> find_canonical_duplicate -> Annotations.annotated_signature -> 'a TypeState.t -> diff --git a/infer/src/eradicate/typeState.ml b/infer/src/eradicate/typeState.ml index 2af09efbe..440645e33 100644 --- a/infer/src/eradicate/typeState.ml +++ b/infer/src/eradicate/typeState.ml @@ -23,7 +23,8 @@ type 'a ext = { empty : 'a; (** empty extension *) check_instr : (** check the extension for an instruction *) - get_proc_desc -> Procname.t -> Cfg.Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a; + Sil.tenv -> get_proc_desc -> Procname.t -> + Cfg.Procdesc.t -> 'a -> Sil.instr -> parameters -> 'a; join : 'a -> 'a -> 'a; (** join two extensions *) pp : Format.formatter -> 'a -> unit (** pretty print an extension *) } diff --git a/infer/src/eradicate/typeState.mli b/infer/src/eradicate/typeState.mli index 1073c9c08..0eb1141d1 100644 --- a/infer/src/eradicate/typeState.mli +++ b/infer/src/eradicate/typeState.mli @@ -19,7 +19,8 @@ type 'a ext = { empty : 'a; (** empty extension *) check_instr : (** check the extension for an instruction *) - get_proc_desc -> Procname.t -> Cfg.Procdesc.t ->'a -> Sil.instr -> parameters -> 'a; + Sil.tenv -> get_proc_desc -> Procname.t -> + Cfg.Procdesc.t ->'a -> Sil.instr -> parameters -> 'a; join : 'a -> 'a -> 'a; (** join two extensions *) pp : Format.formatter -> 'a -> unit (** pretty print an extension *) } diff --git a/infer/src/java/jConfig.ml b/infer/src/java/jConfig.ml index f4ab2f31a..aecff99bc 100644 --- a/infer/src/java/jConfig.ml +++ b/infer/src/java/jConfig.ml @@ -146,7 +146,3 @@ let translate_checks = ref false (* Generate harness for Android code *) let create_harness = ref false - -(* Create a procedure description of callees *) -let create_callee_procdesc = - Config.from_env_variable "INFER_CREATE_CALLEE_PDESC" diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index a1118109b..1342a3915 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -551,11 +551,8 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_ end in loop cn cn in let cn' = resolve_method context cn ms in - let cfg = JContext.get_cfg context in let tenv = JContext.get_tenv context in let program = JContext.get_program context in - if JConfig.create_callee_procdesc then - ignore (get_method_procdesc program cfg tenv cn' ms method_kind); let cf_virtual, cf_interface = match invoke_code with | I_Virtual -> (true, false) | I_Interface -> (true, true)