diff --git a/infer/src/IR/ProcAttributes.ml b/infer/src/IR/ProcAttributes.ml index cb20ce092..39aac9c7d 100644 --- a/infer/src/IR/ProcAttributes.ml +++ b/infer/src/IR/ProcAttributes.ml @@ -57,7 +57,6 @@ type t = ; is_model: bool (** the procedure is a model *) ; is_specialized: bool (** the procedure is a clone specialized for dynamic dispatch handling *) ; is_synthetic_method: bool (** the procedure is a synthetic method *) - ; language: Config.language (** language of the procedure *) ; loc: Location.t (** location of this procedure in the source code *) ; translation_unit: SourceFile.t option (** translation unit to which the procedure belongs *) ; mutable locals: (Mangled.t * Typ.t) list (** name and type of local variables *) @@ -69,7 +68,7 @@ type t = ; source_file_captured: SourceFile.t (** source file where the procedure was captured *) } [@@deriving compare] -let default proc_name language = +let default proc_name = { access= PredSymb.Default ; captured= [] ; changed= true @@ -90,7 +89,6 @@ let default proc_name language = ; is_model= false ; is_specialized= false ; is_synthetic_method= false - ; language ; loc= Location.dummy ; translation_unit= None ; locals= [] @@ -100,4 +98,3 @@ let default proc_name language = ; proc_name ; ret_type= Typ.mk Typ.Tvoid ; source_file_captured= SourceFile.invalid __FILE__ } - diff --git a/infer/src/IR/ProcAttributes.mli b/infer/src/IR/ProcAttributes.mli index cdf8c0445..1adcf01ec 100644 --- a/infer/src/IR/ProcAttributes.mli +++ b/infer/src/IR/ProcAttributes.mli @@ -54,7 +54,6 @@ type t = ; is_model: bool (** the procedure is a model *) ; is_specialized: bool (** the procedure is a clone specialized for dynamic dispatch handling *) ; is_synthetic_method: bool (** the procedure is a synthetic method *) - ; language: Config.language (** language of the procedure *) ; loc: Location.t (** location of this procedure in the source code *) ; translation_unit: SourceFile.t option (** translation unit to which the procedure belongs *) ; mutable locals: (Mangled.t * Typ.t) list (** name and type of local variables *) @@ -66,5 +65,5 @@ type t = ; source_file_captured: SourceFile.t (** source file where the procedure was captured *) } [@@deriving compare] -val default : Typ.Procname.t -> Config.language -> t +val default : Typ.Procname.t -> t (** Create a proc_attributes with default values. *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index ec2ff665d..00cf6a198 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1047,7 +1047,7 @@ let perform_analysis_phase tenv (summary: Specs.summary) (proc_cfg: ProcCfg.Exce let set_current_language proc_desc = - let language = (Procdesc.get_attributes proc_desc).ProcAttributes.language in + let language = Typ.Procname.get_language (Procdesc.get_proc_name proc_desc) in Config.curr_language := language diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index d643433e2..3a058bdd0 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -1005,18 +1005,16 @@ let check_inconsistency_base tenv prop = false | Some (_, _, pdesc) -> let procedure_attr = Procdesc.get_attributes pdesc in - let is_java_this pvar = - Config.equal_language procedure_attr.ProcAttributes.language Config.Java - && Pvar.is_this pvar - in + let language = Typ.Procname.get_language (Procdesc.get_proc_name pdesc) in + let is_java_this pvar = Config.equal_language language Config.Java && Pvar.is_this pvar in let is_objc_instance_self pvar = - Config.equal_language procedure_attr.ProcAttributes.language Config.Clang + Config.equal_language language Config.Clang && Mangled.equal (Pvar.get_name pvar) (Mangled.from_string "self") && procedure_attr.ProcAttributes.is_objc_instance_method in let is_cpp_this pvar = - Config.equal_language procedure_attr.ProcAttributes.language Config.Clang - && Pvar.is_this pvar && procedure_attr.ProcAttributes.is_cpp_instance_method + Config.equal_language language Config.Clang && Pvar.is_this pvar + && procedure_attr.ProcAttributes.is_cpp_instance_method in let do_hpred = function | Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) -> diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index ddaeb11e4..9eaecfcb0 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -772,7 +772,7 @@ let init_summary (nodes, calls, proc_desc) = let dummy = - let dummy_attributes = ProcAttributes.default Typ.Procname.empty_block Config.Java in + let dummy_attributes = ProcAttributes.default Typ.Procname.empty_block in let dummy_proc_desc = Procdesc.from_proc_attributes ~called_from_cfg:true dummy_attributes in init_summary ([], [], dummy_proc_desc) @@ -781,12 +781,3 @@ let dummy = let reset_summary proc_desc = init_summary ([], [], proc_desc) (* =============== END of support for spec tables =============== *) -(* -let rec post_equal pl1 pl2 = match pl1, pl2 with - | [],[] -> true - | [], _:: _ -> false - | _:: _,[] -> false - | p1:: pl1', p2:: pl2' -> - if Prop.equal_prop p1 p2 then post_equal pl1' pl2' - else false -*) diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 81833a925..c9d8d4229 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -600,7 +600,7 @@ let create_local_procdesc ?(set_objc_accessor_attr= false) trans_unit_ctx cfg te in let procdesc = let proc_attributes = - { (ProcAttributes.default proc_name Config.Clang) with + { (ProcAttributes.default proc_name) with ProcAttributes.captured= captured_mangled ; formals ; const_formals @@ -648,7 +648,7 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt = (Typ.mk Typ.Tvoid, []) in let proc_attributes = - { (ProcAttributes.default proc_name Config.Clang) with + { (ProcAttributes.default proc_name) with ProcAttributes.formals; is_objc_instance_method= is_objc_inst_method; ret_type } in ignore (Cfg.create_proc_desc cfg proc_attributes) @@ -694,4 +694,3 @@ let get_captures_from_cpp_lambda dec = cxx_rdi.xrdi_lambda_captures | _ -> assert false - diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 0e8dcece1..fc7d78371 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -555,8 +555,7 @@ let typecheck_instr tenv ext calls_this checks (node: Procdesc.Node.t) idenv get in let ret_type = Typ.java_proc_return_typ callee_pname_java in let proc_attributes = - { (ProcAttributes.default callee_pname Config.Java) with - ProcAttributes.formals; ret_type } + {(ProcAttributes.default callee_pname) with ProcAttributes.formals; ret_type} in proc_attributes in diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index f33d08250..f5ce07f1c 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -306,7 +306,7 @@ let create_am_procdesc source_file program icfg am proc_name : Procdesc.t = let method_annotation = JAnnotation.translate_method am.Javalib.am_annotations in let procdesc = let proc_attributes = - { (ProcAttributes.default proc_name Config.Java) with + { (ProcAttributes.default proc_name) with ProcAttributes.access= trans_access am.Javalib.am_access ; exceptions= List.map ~f:JBasics.cn_name am.Javalib.am_exceptions ; formals @@ -332,7 +332,7 @@ let create_native_procdesc source_file program icfg cm proc_name = let method_annotation = JAnnotation.translate_method cm.Javalib.cm_annotations in let procdesc = let proc_attributes = - { (ProcAttributes.default proc_name Config.Java) with + { (ProcAttributes.default proc_name) with ProcAttributes.access= trans_access cm.Javalib.cm_access ; exceptions= List.map ~f:JBasics.cn_name cm.Javalib.cm_exceptions ; formals @@ -368,7 +368,7 @@ let create_cm_procdesc source_file program linereader icfg cm proc_name skip_imp update_constr_loc cn ms loc_start ; update_init_loc cn ms loc_exit ; let proc_attributes = - { (ProcAttributes.default proc_name Config.Java) with + { (ProcAttributes.default proc_name) with ProcAttributes.access= trans_access cm.Javalib.cm_access ; exceptions= List.map ~f:JBasics.cn_name cm.Javalib.cm_exceptions ; formals @@ -1124,4 +1124,3 @@ let instruction (context: JContext.t) pc instr : translation = with Frontend_error s -> L.internal_error "Skipping because of: %s@." s ; Skip - diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index c6ce23baf..3bbe6b833 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -171,9 +171,7 @@ struct let structured_program_to_cfg program test_pname = let cfg = Cfg.create_cfg () in - let pdesc = - Cfg.create_proc_desc cfg (ProcAttributes.default test_pname !Config.curr_language) - in + let pdesc = Cfg.create_proc_desc cfg (ProcAttributes.default test_pname) in let pname = Procdesc.get_proc_name pdesc in let create_node kind cmds = Procdesc.create_node pdesc dummy_loc kind cmds in let set_succs cur_node succs ~exn_handlers = diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index 164fbaa8c..567f182fe 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -15,10 +15,7 @@ module BackwardInstrCfg = ProcCfg.Backward (InstrCfg) let tests = let cfg = Cfg.create_cfg () in - let test_pdesc = - Cfg.create_proc_desc cfg - (ProcAttributes.default Typ.Procname.empty_block !Config.curr_language) - in + let test_pdesc = Cfg.create_proc_desc cfg (ProcAttributes.default Typ.Procname.empty_block) in let dummy_instr1 = Sil.Remove_temps ([], Location.dummy) in let dummy_instr2 = Sil.Abstract Location.dummy in let dummy_instr3 = Sil.Remove_temps ([Ident.create_fresh Ident.knormal], Location.dummy) in