From e7d0038af39a13ea93c481b5065362dff0dd4302 Mon Sep 17 00:00:00 2001 From: jrm Date: Fri, 26 Jun 2015 22:07:43 -0700 Subject: [PATCH] [infer] fix OCaml formatting --- infer/src/backend/procname.ml | 8 ++-- infer/src/backend/sil.ml | 8 ++-- infer/src/backend/specs.ml | 8 ++-- infer/src/backend/symExec.ml | 90 +++++++++++++++++------------------ 4 files changed, 57 insertions(+), 57 deletions(-) diff --git a/infer/src/backend/procname.ml b/infer/src/backend/procname.ml index cd55d7b73..d350be066 100644 --- a/infer/src/backend/procname.ml +++ b/infer/src/backend/procname.ml @@ -317,11 +317,11 @@ let is_class_initializer = function (** [is_infer_undefined pn] returns true if [pn] is a special Infer undefined proc *) let is_infer_undefined pn = match pn with | JAVA j -> - let regexp = Str.regexp "com.facebook.infer.models.InferUndefined" in - Str.string_match regexp (java_get_class pn) 0 + let regexp = Str.regexp "com.facebook.infer.models.InferUndefined" in + Str.string_match regexp (java_get_class pn) 0 | _ -> - (* TODO: add cases for obj-c, c, c++ *) - false + (* TODO: add cases for obj-c, c, c++ *) + false (** to_string for C_CPP and STATIC types *) let to_readable_string (c1, c2) verbose = diff --git a/infer/src/backend/sil.ml b/infer/src/backend/sil.ml index 2c9582b03..5e97a0ecd 100644 --- a/infer/src/backend/sil.ml +++ b/infer/src/backend/sil.ml @@ -151,7 +151,7 @@ type pvar_kind = | Callee_var of Procname.t (** local variable belonging to a callee *) | Abducted_retvar of Procname.t * location (** synthetic variable to represent return value *) | Abducted_ref_param of Procname.t * pvar * location - (** synthetic variable to represent param passed by reference *) + (** synthetic variable to represent param passed by reference *) | Global_var (** gloval variable *) | Seed_var (** variable used to store the initial value of formal parameters *) @@ -667,8 +667,8 @@ and attribute = | Adiv0 of path_pos (** value appeared in second argument of division in path position *) | Aobjc_null of exp (** the exp. is null because of a call to a method with exp as a null receiver *) | Avariadic_function_argument of Procname.t * int * int (** (pn, n, i) the exp. is used as [i]th - argument of a call to the variadic - function [pn] that has [n] arguments *) + argument of a call to the variadic + function [pn] that has [n] arguments *) | Aretval of Procname.t (** value was returned from a call to the given procedure *) (** Categories of attributes *) @@ -1812,7 +1812,7 @@ let pp_pvar_latex f pv = | Abducted_retvar (n, l) -> F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) (Latex.pp_string Latex.Roman) "abductedRetvar" - | Abducted_ref_param (n, pv, l) -> + | Abducted_ref_param (n, pv, l) -> F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name) (Latex.pp_string Latex.Roman) "abductedRefParam" | Global_var -> diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 1350cac1a..753955413 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -560,8 +560,8 @@ let load_summary_to_spec_table proc_name = true in let load_summary_models models_dir = match load_summary models_dir with - | None -> false - | Some summ -> add summ Models in + | None -> false + | Some summ -> add summ Models in let rec load_summary_libs = function (* try to load the summary from a list of libs *) | [] -> false | spec_path :: spec_paths -> @@ -587,11 +587,11 @@ let load_summary_to_spec_table proc_name = let default_spec_dir = res_dir_specs_filename proc_name in match load_summary default_spec_dir with | None -> - (* search on models, libzips, and libs *) + (* search on models, libzips, and libs *) if load_summary_models (specs_models_filename proc_name) then true else if load_summary_ziplibs !Config.zip_libraries then true else load_summary_libs (specs_library_filenames proc_name) - + | Some summ -> add summ Res_dir diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index a078bc68a..b6c7b1c2e 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1047,41 +1047,41 @@ and add_constraints_on_retval pdesc prop ret_ids ret_type_option callee_pname = else match ret_ids, ret_type_option with | [ret_id], Some ret_typ -> - (* To avoid obvious false positives, assume skip functions do not return null pointers *) - let add_ret_non_null ret_id ret_typ prop = - match ret_typ with - | Sil.Tptr _ -> Prop.conjoin_neq (Sil.Var ret_id) Sil.exp_zero prop - | _ -> prop in - let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *) - Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in - if !Config.angelic_execution && not (is_rec_call callee_pname) then - (* introduce a fresh program variable to allow abduction on the return value *) - let abducted_ret_pv = Sil.mk_pvar_abducted_ret callee_pname (State.get_loc ()) in - let already_has_abducted_retval p = - list_exists - (fun hpred -> match hpred with - | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ret_pv - | _ -> false) - (Prop.get_sigma_footprint p) in + (* To avoid obvious false positives, assume skip functions do not return null pointers *) + let add_ret_non_null ret_id ret_typ prop = + match ret_typ with + | Sil.Tptr _ -> Prop.conjoin_neq (Sil.Var ret_id) Sil.exp_zero prop + | _ -> prop in + let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *) + Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in + if !Config.angelic_execution && not (is_rec_call callee_pname) then + (* introduce a fresh program variable to allow abduction on the return value *) + let abducted_ret_pv = Sil.mk_pvar_abducted_ret callee_pname (State.get_loc ()) in + let already_has_abducted_retval p = + list_exists + (fun hpred -> match hpred with + | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ret_pv + | _ -> false) + (Prop.get_sigma_footprint p) in (* prevent introducing multiple abducted retvals for a single call site in a loop *) - if already_has_abducted_retval prop then prop - else + if already_has_abducted_retval prop then prop + else if !Config.footprint then let (prop', fresh_fp_var) = add_to_footprint abducted_ret_pv ret_typ prop in - let prop'' = Prop.conjoin_eq ~footprint:true (Sil.Var ret_id) fresh_fp_var prop' in + let prop'' = Prop.conjoin_eq ~footprint: true (Sil.Var ret_id) fresh_fp_var prop' in add_ret_non_null ret_id ret_typ prop'' else (* find an hpred [abducted_pvar] |-> A in [prop] and add [exp] = A to prop *) let bind_exp_to_abducted_val exp_to_bind abducted_pvar prop = let bind_exp prop = function | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _) - when Sil.pvar_equal pv abducted_pvar -> - Prop.conjoin_eq exp_to_bind rhs prop + when Sil.pvar_equal pv abducted_pvar -> + Prop.conjoin_eq exp_to_bind rhs prop | _ -> prop in list_fold_left bind_exp prop (Prop.get_sigma prop) in (* bind return id to the abducted value pointed to by the pvar we introduced *) bind_exp_to_abducted_val (Sil.Var ret_id) abducted_ret_pv prop - else add_ret_non_null ret_id ret_typ prop + else add_ret_non_null ret_id ret_typ prop | _ -> prop and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname = @@ -1098,18 +1098,18 @@ and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname = let add_actual_by_ref_to_footprint prop (actual, actual_typ) = match actual with | Sil.Lvar actual_pv -> - (* introduce a fresh program variable to allow abduction on the return value *) - let abducted_ref_pv = - Sil.mk_pvar_abducted_ref_param callee_pname actual_pv (State.get_loc ()) in - let already_has_abducted_retval p = - list_exists - (fun hpred -> match hpred with - | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ref_pv - | _ -> false) - (Prop.get_sigma_footprint p) in + (* introduce a fresh program variable to allow abduction on the return value *) + let abducted_ref_pv = + Sil.mk_pvar_abducted_ref_param callee_pname actual_pv (State.get_loc ()) in + let already_has_abducted_retval p = + list_exists + (fun hpred -> match hpred with + | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ref_pv + | _ -> false) + (Prop.get_sigma_footprint p) in (* prevent introducing multiple abducted retvals for a single call site in a loop *) - if already_has_abducted_retval prop then prop - else + if already_has_abducted_retval prop then prop + else if !Config.footprint then let (prop', fresh_fp_var) = add_to_footprint abducted_ref_pv (Sil.typ_strip_ptr actual_typ) prop in @@ -1118,7 +1118,7 @@ and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname = list_map (function | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual -> - Sil.Hpointsto (lhs, Sil.Eexp (fresh_fp_var, Sil.Inone), typ_exp) + Sil.Hpointsto (lhs, Sil.Eexp (fresh_fp_var, Sil.Inone), typ_exp) | hpred -> hpred) (Prop.get_sigma prop') in Prop.normalize (Prop.replace_sigma filtered_sigma prop') @@ -1127,19 +1127,19 @@ and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname = let prop' = let filtered_sigma = list_filter - (function - | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual -> - false - | _ -> true) - (Prop.get_sigma prop) in + (function + | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual -> + false + | _ -> true) + (Prop.get_sigma prop) in Prop.normalize (Prop.replace_sigma filtered_sigma prop) in list_fold_left (fun p hpred -> - match hpred with - | Sil.Hpointsto (Sil.Lvar pv, rhs, texp) when Sil.pvar_equal pv abducted_ref_pv -> - let new_hpred = Sil.Hpointsto (actual, rhs, texp) in - Prop.normalize (Prop.replace_sigma (new_hpred :: (Prop.get_sigma prop')) p) - | _ -> p) + match hpred with + | Sil.Hpointsto (Sil.Lvar pv, rhs, texp) when Sil.pvar_equal pv abducted_ref_pv -> + let new_hpred = Sil.Hpointsto (actual, rhs, texp) in + Prop.normalize (Prop.replace_sigma (new_hpred :: (Prop.get_sigma prop')) p) + | _ -> p) prop' (Prop.get_sigma prop') | _ -> assert false in @@ -1161,7 +1161,7 @@ and call_unknown_or_scan is_scan cfg pdesc tenv pre path let do_exp p (e, t) = let do_attribute q = function | Sil.Aresource _ as res -> - Prop.remove_attribute res q + Prop.remove_attribute res q | _ -> q in list_fold_left do_attribute p (Prop.get_exp_attributes p e) in list_fold_left do_exp prop actual_pars in