pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[infer] fix OCaml formatting

Browse Source
master
jrm 10 years ago
parent af730cd16d
commit e7d0038af3
4 changed files with 57 additions and 57 deletions
Show Stats Download Patch File Download Diff File

8
infer/src/backend/procname.ml
Unescape View File

@ -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 =

8
infer/src/backend/sil.ml
Unescape View File

@ -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 ->

8
infer/src/backend/specs.ml
Unescape View File

@ -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

90
infer/src/backend/symExec.ml
Unescape View File

@ -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

Write Preview
Loading…
Cancel
Save