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

[caml] 4.12 is fussier about possible name ambiguities

Browse Source 
Summary: Fix warnings ahead of OCaml upgrade.

Reviewed By: ngorogiannis

Differential Revision: D28870887

fbshipit-source-id: 6682bbb6e
master
Jules Villard 4 years ago committed by Facebook GitHub Bot
parent cfed4c4fa0
commit 4e3afbe329
13 changed files with 82 additions and 82 deletions
Show Stats Download Patch File Download Diff File

28
infer/src/absint/HilExp.ml
Unescape View File

@ -432,8 +432,8 @@ let rec array_index_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp t
and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp0 typ0 = and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp0 typ0 =
let rec of_exp_ exp typ (add_accesses : AccessExpression.t -> AccessExpression.t) acc : let rec of_exp_ exp typ (add_accesses : AccessExpression.t -> AccessExpression.t) acc :
AccessExpression.t list = AccessExpression.t list =
match exp with match (exp : Exp.t) with
| Exp.Var id -> ( | Var id -> (
match f_resolve_id (Var.of_id id) with match f_resolve_id (Var.of_id id) with
| Some access_expr -> | Some access_expr ->
let access_expr' = let access_expr' =
@ -446,7 +446,7 @@ and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp0 typ
if add_deref then AccessExpression.dereference access_expr else access_expr if add_deref then AccessExpression.dereference access_expr else access_expr
in in
add_accesses access_expr' :: acc ) add_accesses access_expr' :: acc )
| Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> ( | Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> (
match f_resolve_id (Var.of_pvar pvar) with match f_resolve_id (Var.of_pvar pvar) with
| Some access_expr -> | Some access_expr ->
(* do not need to add deref here as it was added implicitly in the binding *) (* do not need to add deref here as it was added implicitly in the binding *)
@ -462,18 +462,18 @@ and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp0 typ
if add_deref then AccessExpression.dereference access_expr else access_expr if add_deref then AccessExpression.dereference access_expr else access_expr
in in
add_accesses access_expr' :: acc ) add_accesses access_expr' :: acc )
| Exp.Lvar pvar -> | Lvar pvar ->
let access_expr = AccessExpression.of_pvar pvar typ in let access_expr = AccessExpression.of_pvar pvar typ in
let access_expr' = let access_expr' =
if add_deref then AccessExpression.dereference access_expr else access_expr if add_deref then AccessExpression.dereference access_expr else access_expr
in in
add_accesses access_expr' :: acc add_accesses access_expr' :: acc
| Exp.Lfield (root_exp, fld, root_exp_typ) -> | Lfield (root_exp, fld, root_exp_typ) ->
let add_field_access_expr access_expr = let add_field_access_expr access_expr =
add_accesses (AccessExpression.field_offset access_expr fld) add_accesses (AccessExpression.field_offset access_expr fld)
in in
of_exp_ root_exp root_exp_typ add_field_access_expr acc of_exp_ root_exp root_exp_typ add_field_access_expr acc
| Exp.Lindex (root_exp, index_exp) -> | Lindex (root_exp, index_exp) ->
let index = let index =
let index_typ = (* TODO: bogus *) StdTyp.void in let index_typ = (* TODO: bogus *) StdTyp.void in
array_index_of_exp ~include_array_indexes ~f_resolve_id ~add_deref index_exp index_typ array_index_of_exp ~include_array_indexes ~f_resolve_id ~add_deref index_exp index_typ
@ -483,28 +483,28 @@ and access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref exp0 typ
in in
let array_typ = Typ.mk_array typ in let array_typ = Typ.mk_array typ in
of_exp_ root_exp array_typ add_array_access_expr acc of_exp_ root_exp array_typ add_array_access_expr acc
| Exp.Cast (cast_typ, cast_exp) -> | Cast (cast_typ, cast_exp) ->
of_exp_ cast_exp cast_typ Fn.id acc of_exp_ cast_exp cast_typ Fn.id acc
| Exp.UnOp (_, unop_exp, _) -> | UnOp (_, unop_exp, _) ->
of_exp_ unop_exp typ Fn.id acc of_exp_ unop_exp typ Fn.id acc
| Exp.Exn exn_exp -> | Exn exn_exp ->
of_exp_ exn_exp typ Fn.id acc of_exp_ exn_exp typ Fn.id acc
| Exp.BinOp (_, exp1, exp2) -> | BinOp (_, exp1, exp2) ->
of_exp_ exp1 typ Fn.id acc |> of_exp_ exp2 typ Fn.id of_exp_ exp1 typ Fn.id acc |> of_exp_ exp2 typ Fn.id
| Exp.Const _ | Closure _ | Sizeof _ -> | Const _ | Closure _ | Sizeof _ ->
acc acc
in in
of_exp_ exp0 typ0 Fn.id [] of_exp_ exp0 typ0 Fn.id []
and access_expr_of_lhs_exp ~include_array_indexes ~f_resolve_id ~add_deref lhs_exp typ = and access_expr_of_lhs_exp ~include_array_indexes ~f_resolve_id ~add_deref lhs_exp typ =
match lhs_exp with match (lhs_exp : Exp.t) with
| Exp.Lfield _ when not add_deref -> ( | Lfield _ when not add_deref -> (
let res = let res =
access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref:true lhs_exp typ access_exprs_of_exp ~include_array_indexes ~f_resolve_id ~add_deref:true lhs_exp typ
in in
match res with [lhs_ae] -> AccessExpression.address_of lhs_ae | _ -> None ) match res with [lhs_ae] -> AccessExpression.address_of lhs_ae | _ -> None )
| Exp.Lindex _ when not add_deref -> ( | Lindex _ when not add_deref -> (
let res = let res =
let typ' = let typ' =
match typ.Typ.desc with match typ.Typ.desc with

14
infer/src/backend/preanal.ml
Unescape View File

@ -326,12 +326,12 @@ module Liveness = struct
let is_last_instr_in_node instr node = phys_equal (last_instr_in_node node) instr let is_last_instr_in_node instr node = phys_equal (last_instr_in_node node) instr
let exec_instr ((active_defs, to_nullify) as astate) extras node _ instr = let exec_instr ((active_defs, to_nullify) as astate) extras node _ (instr : Sil.instr) =
let astate' = let astate' =
match instr with match instr with
| Sil.Load {id= lhs_id} -> | Load {id= lhs_id} ->
(VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify) (VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify)
| Sil.Call ((id, _), _, actuals, _, {CallFlags.cf_assign_last_arg}) -> | Call ((id, _), _, actuals, _, {CallFlags.cf_assign_last_arg}) ->
let active_defs = VarDomain.add (Var.of_id id) active_defs in let active_defs = VarDomain.add (Var.of_id id) active_defs in
let active_defs = let active_defs =
if cf_assign_last_arg then if cf_assign_last_arg then
@ -343,15 +343,15 @@ module Liveness = struct
else active_defs else active_defs
in in
(active_defs, to_nullify) (active_defs, to_nullify)
| Sil.Store {e1= Exp.Lvar lhs_pvar} -> | Store {e1= Exp.Lvar lhs_pvar} ->
(VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify) (VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify)
| Sil.Metadata (VariableLifetimeBegins (pvar, _, _)) -> | Metadata (VariableLifetimeBegins (pvar, _, _)) ->
(VarDomain.add (Var.of_pvar pvar) active_defs, to_nullify) (VarDomain.add (Var.of_pvar pvar) active_defs, to_nullify)
| Sil.Store _ | Store _
| Prune _ | Prune _
| Metadata (Abstract _ | CatchEntry _ | ExitScope _ | Skip | TryEntry _ | TryExit _) -> | Metadata (Abstract _ | CatchEntry _ | ExitScope _ | Skip | TryEntry _ | TryExit _) ->
astate astate
| Sil.Metadata (Nullify _) -> | Metadata (Nullify _) ->
L.(die InternalError) L.(die InternalError)
"Should not add nullify instructions before running nullify analysis!" "Should not add nullify instructions before running nullify analysis!"
in in

2
infer/src/biabduction/Abs.ml
Unescape View File

@ -935,7 +935,7 @@ let abstract_gc tenv p =
let strong_filter = function let strong_filter = function
| Predicates.Aeq (e1, e2) | Predicates.Aneq (e1, e2) -> | Predicates.Aeq (e1, e2) | Predicates.Aneq (e1, e2) ->
check (Exp.free_vars e1) && check (Exp.free_vars e2) check (Exp.free_vars e1) && check (Exp.free_vars e2)
| (Predicates.Apred _ | Anpred _) as a -> | Predicates.(Apred _ | Anpred _) as a ->
check (Predicates.atom_free_vars a) check (Predicates.atom_free_vars a)
in in
let new_pi = List.filter ~f:strong_filter pi in let new_pi = List.filter ~f:strong_filter pi in

18
infer/src/biabduction/Attribute.ml
Unescape View File

@ -11,7 +11,7 @@ open! IStd
(** Attribute manipulation in Propositions (i.e., Symbolic Heaps) *) (** Attribute manipulation in Propositions (i.e., Symbolic Heaps) *)
(** Check whether an atom is used to mark an attribute *) (** Check whether an atom is used to mark an attribute *)
let is_pred atom = match atom with Predicates.Apred _ | Anpred _ -> true | _ -> false let is_pred atom = match atom with Predicates.(Apred _ | Anpred _) -> true | _ -> false
(** Add an attribute associated to the argument expressions *) (** Add an attribute associated to the argument expressions *)
let add tenv ?(footprint = false) ?(polarity = true) prop attr args = let add tenv ?(footprint = false) ?(polarity = true) prop attr args =
@ -27,13 +27,13 @@ let attributes_in_same_category attr1 attr2 =
(** Replace an attribute associated to the expression *) (** Replace an attribute associated to the expression *)
let add_or_replace_check_changed tenv prop atom = let add_or_replace_check_changed tenv prop atom =
match atom with match (atom : Predicates.atom) with
| Predicates.Apred (att0, (_ :: _ as exps0)) | Anpred (att0, (_ :: _ as exps0)) -> | Apred (att0, (_ :: _ as exps0)) | Anpred (att0, (_ :: _ as exps0)) ->
let pairs = List.map ~f:(fun e -> (e, Prop.exp_normalize_prop tenv prop e)) exps0 in let pairs = List.map ~f:(fun e -> (e, Prop.exp_normalize_prop tenv prop e)) exps0 in
let _, nexp = List.hd_exn pairs in let _, nexp = List.hd_exn pairs in
(* len exps0 > 0 by match *) (* len exps0 > 0 by match *)
let atom_map = function let atom_map = function
| (Predicates.Apred (att, exp :: _) | Anpred (att, exp :: _)) | Predicates.(Apred (att, exp :: _) | Anpred (att, exp :: _))
when Exp.equal nexp exp && attributes_in_same_category att att0 -> when Exp.equal nexp exp && attributes_in_same_category att att0 ->
atom atom
| atom' -> | atom' ->
@ -64,8 +64,8 @@ let get_all (prop : 'a Prop.t) =
let get_for_exp tenv (prop : 'a Prop.t) exp = let get_for_exp tenv (prop : 'a Prop.t) exp =
let nexp = Prop.exp_normalize_prop tenv prop exp in let nexp = Prop.exp_normalize_prop tenv prop exp in
let atom_get_attr attributes atom = let atom_get_attr attributes atom =
match atom with match (atom : Predicates.atom) with
| (Predicates.Apred (_, es) | Anpred (_, es)) when List.mem ~equal:Exp.equal es nexp -> | (Apred (_, es) | Anpred (_, es)) when List.mem ~equal:Exp.equal es nexp ->
atom :: attributes atom :: attributes
| _ -> | _ ->
attributes attributes
@ -77,7 +77,7 @@ let get tenv prop exp category =
let atts = get_for_exp tenv prop exp in let atts = get_for_exp tenv prop exp in
List.find List.find
~f:(function ~f:(function
| Predicates.Apred (att, _) | Anpred (att, _) -> | Predicates.(Apred (att, _) | Anpred (att, _)) ->
PredSymb.equal_category (PredSymb.to_category att) category PredSymb.equal_category (PredSymb.to_category att) category
| _ -> | _ ->
false ) false )
@ -118,7 +118,7 @@ let remove tenv prop atom =
(** Remove an attribute from all the atoms in the heap *) (** Remove an attribute from all the atoms in the heap *)
let remove_for_attr tenv prop att0 = let remove_for_attr tenv prop att0 =
let f = function let f = function
| Predicates.Apred (att, _) | Anpred (att, _) -> | Predicates.(Apred (att, _) | Anpred (att, _)) ->
not (PredSymb.equal att0 att) not (PredSymb.equal att0 att)
| _ -> | _ ->
true true
@ -196,7 +196,7 @@ let mark_vars_as_undefined tenv prop ~ret_exp ~undefined_actuals_by_ref callee_p
path_pos = path_pos =
let mark_var_as_undefined ~annot exp prop = let mark_var_as_undefined ~annot exp prop =
match exp with match exp with
| Exp.Var _ | Lvar _ -> | Exp.(Var _ | Lvar _) ->
let att_undef = PredSymb.Aundef (callee_pname, annot, loc, path_pos) in let att_undef = PredSymb.Aundef (callee_pname, annot, loc, path_pos) in
add_or_replace tenv prop (Apred (att_undef, [exp])) add_or_replace tenv prop (Apred (att_undef, [exp]))
| _ -> | _ ->

17
infer/src/biabduction/Prover.ml
Unescape View File

@ -963,16 +963,17 @@ let check_inconsistency_base tenv prop =
in in
List.exists ~f:do_hpred sigma List.exists ~f:do_hpred sigma
in in
let inconsistent_atom = function let inconsistent_atom (atom : Predicates.atom) =
| Predicates.Aeq (e1, e2) -> ( match atom with
| Aeq (e1, e2) -> (
match (e1, e2) with match (e1, e2) with
| Exp.Const c1, Exp.Const c2 -> | Exp.Const c1, Exp.Const c2 ->
not (Const.equal c1 c2) not (Const.equal c1 c2)
| _ -> | _ ->
check_disequal tenv prop e1 e2 ) check_disequal tenv prop e1 e2 )
| Predicates.Aneq (e1, e2) -> ( | Aneq (e1, e2) -> (
match (e1, e2) with Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2 | _ -> Exp.equal e1 e2 ) match (e1, e2) with Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2 | _ -> Exp.equal e1 e2 )
| Predicates.Apred _ | Anpred _ -> | Apred _ | Anpred _ ->
false false
in in
let inconsistent_inequalities () = let inconsistent_inequalities () =
@ -2390,10 +2391,10 @@ let imply_atom tenv calc_missing (sub1, sub2) prop a =
(** Check pure implications before looking at the spatial part. Add necessary instantiations for (** Check pure implications before looking at the spatial part. Add necessary instantiations for
equalities and check that instantiations are possible for disequalities. *) equalities and check that instantiations are possible for disequalities. *)
let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 = let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
match pi2 with match (pi2 : Predicates.atom list) with
| [] -> | [] ->
subs subs
| (Predicates.Aeq (e2_in, f2_in) as a) :: pi2' when not (Prop.atom_is_inequality a) -> ( | (Aeq (e2_in, f2_in) as a) :: pi2' when not (Prop.atom_is_inequality a) -> (
let e2, f2 = (Predicates.exp_sub (snd subs) e2_in, Predicates.exp_sub (snd subs) f2_in) in let e2, f2 = (Predicates.exp_sub (snd subs) e2_in, Predicates.exp_sub (snd subs) f2_in) in
if Exp.equal e2 f2 then pre_check_pure_implication tenv calc_missing subs pi1 pi2' if Exp.equal e2 f2 then pre_check_pure_implication tenv calc_missing subs pi1 pi2'
else else
@ -2411,14 +2412,14 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 =
let prop_for_impl = prepare_prop_for_implication tenv subs pi1' [] in let prop_for_impl = prepare_prop_for_implication tenv subs pi1' [] in
imply_atom tenv calc_missing subs prop_for_impl (Predicates.Aeq (e2_in, f2_in)) ; imply_atom tenv calc_missing subs prop_for_impl (Predicates.Aeq (e2_in, f2_in)) ;
pre_check_pure_implication tenv calc_missing subs pi1 pi2' ) pre_check_pure_implication tenv calc_missing subs pi1 pi2' )
| (Predicates.Aneq (e, _) | Apred (_, e :: _) | Anpred (_, e :: _)) :: _ | (Aneq (e, _) | Apred (_, e :: _) | Anpred (_, e :: _)) :: _
when (not calc_missing) && match e with Var v -> not (Ident.is_primed v) | _ -> true -> when (not calc_missing) && match e with Var v -> not (Ident.is_primed v) | _ -> true ->
raise raise
(IMPL_EXC (IMPL_EXC
( "ineq e2=f2 in rhs with e2 not primed var" ( "ineq e2=f2 in rhs with e2 not primed var"
, (Predicates.sub_empty, Predicates.sub_empty) , (Predicates.sub_empty, Predicates.sub_empty)
, EXC_FALSE )) , EXC_FALSE ))
| (Predicates.Aeq _ | Aneq _ | Apred _ | Anpred _) :: pi2' -> | (Aeq _ | Aneq _ | Apred _ | Anpred _) :: pi2' ->
pre_check_pure_implication tenv calc_missing subs pi1 pi2' pre_check_pure_implication tenv calc_missing subs pi1 pi2'

9
infer/src/bufferoverrun/absLoc.ml
Unescape View File

@ -252,12 +252,13 @@ module Loc = struct
false false
let rec is_pretty = function let rec is_pretty (field : _ BoField.t) =
| BoField.Prim (Var _) -> match field with
| Prim (Var _) ->
true true
| BoField.Prim (Allocsite a) -> | Prim (Allocsite a) ->
Allocsite.is_pretty a Allocsite.is_pretty a
| BoField.Field {prefix= loc} | StarField {prefix= loc} -> | Field {prefix= loc} | StarField {prefix= loc} ->
is_pretty loc is_pretty loc

24
infer/src/checkers/addressTaken.ml
Unescape View File

@ -19,26 +19,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
type analysis_data = unit type analysis_data = unit
let rec add_address_taken_pvars exp astate = let rec add_address_taken_pvars (exp : Exp.t) astate =
match exp with match exp with
| Exp.Lvar pvar -> | Lvar pvar ->
Domain.add pvar astate Domain.add pvar astate
| Exp.Cast (_, e) | UnOp (_, e, _) | Lfield (e, _, _) -> | Cast (_, e) | UnOp (_, e, _) | Lfield (e, _, _) ->
add_address_taken_pvars e astate add_address_taken_pvars e astate
| Exp.BinOp (_, e1, e2) | Lindex (e1, e2) -> | BinOp (_, e1, e2) | Lindex (e1, e2) ->
add_address_taken_pvars e1 astate |> add_address_taken_pvars e2 add_address_taken_pvars e1 astate |> add_address_taken_pvars e2
| Exp.Exn _ | Exn _ | Closure _ | Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _) | Var _ | Sizeof _
| Exp.Closure _ ->
| Exp.Const (Cint _ | Cfun _ | Cstr _ | Cfloat _ | Cclass _)
| Exp.Var _
| Exp.Sizeof _ ->
astate astate
let exec_instr astate () _ _ = function let exec_instr astate () _ _ (instr : Sil.instr) =
| Sil.Store {typ= {desc= Tptr _}; e2= rhs_exp} -> match instr with
| Store {typ= {desc= Tptr _}; e2= rhs_exp} ->
add_address_taken_pvars rhs_exp astate add_address_taken_pvars rhs_exp astate
| Sil.Call (_, _, actuals, _, _) -> | Call (_, _, actuals, _, _) ->
let add_actual_by_ref astate_acc = function let add_actual_by_ref astate_acc = function
| actual_exp, {Typ.desc= Tptr _} -> | actual_exp, {Typ.desc= Tptr _} ->
add_address_taken_pvars actual_exp astate_acc add_address_taken_pvars actual_exp astate_acc
@ -46,7 +44,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate_acc astate_acc
in in
List.fold ~f:add_actual_by_ref ~init:astate actuals List.fold ~f:add_actual_by_ref ~init:astate actuals
| Sil.Store _ | Load _ | Prune _ | Metadata _ -> | Store _ | Load _ | Prune _ | Metadata _ ->
astate astate

11
infer/src/checkers/functionPointers.ml
Unescape View File

@ -16,19 +16,20 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
type analysis_data = unit type analysis_data = unit
let exec_instr astate () _ _ = function let exec_instr astate () _ _ (instr : Sil.instr) =
| Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> match instr with
| Load {id= lhs_id} when Ident.is_none lhs_id ->
astate astate
| Sil.Load {id= lhs_id; e= Exp.Lvar rhs_pvar; typ= Typ.{desc= Tptr ({desc= Tfun}, _)}} -> | Load {id= lhs_id; e= Exp.Lvar rhs_pvar; typ= Typ.{desc= Tptr ({desc= Tfun}, _)}} ->
let fun_ptr = let fun_ptr =
try Domain.find (Pvar.to_string rhs_pvar) astate try Domain.find (Pvar.to_string rhs_pvar) astate
with Caml.Not_found -> ProcnameSet.empty with Caml.Not_found -> ProcnameSet.empty
in in
Domain.add (Ident.to_string lhs_id) fun_ptr astate Domain.add (Ident.to_string lhs_id) fun_ptr astate
| Sil.Store {e1= Lvar lhs_pvar; e2= Exp.Const (Const.Cfun pn)} -> | Store {e1= Lvar lhs_pvar; e2= Exp.Const (Const.Cfun pn)} ->
(* strong update *) (* strong update *)
Domain.add (Pvar.to_string lhs_pvar) (ProcnameSet.singleton pn) astate Domain.add (Pvar.to_string lhs_pvar) (ProcnameSet.singleton pn) astate
| Sil.Load _ | Store _ | Call _ | Prune _ | Metadata _ -> | Load _ | Store _ | Call _ | Prune _ | Metadata _ ->
astate astate

5
infer/src/clang/cGeneral_utils.ml
Unescape View File

@ -107,9 +107,10 @@ let is_type_pod qt =
| _ -> | _ ->
None ) None )
|> Option.value_map ~default:true ~f:(function |> Option.value_map ~default:true ~f:(function
| Clang_ast_t.CXXRecordDecl (_, _, _, _, _, _, _, {xrdi_is_pod}) | Clang_ast_t.(
( CXXRecordDecl (_, _, _, _, _, _, _, {xrdi_is_pod})
| ClassTemplateSpecializationDecl (_, _, _, _, _, _, _, {xrdi_is_pod}, _, _) | ClassTemplateSpecializationDecl (_, _, _, _, _, _, _, {xrdi_is_pod}, _, _)
| ClassTemplatePartialSpecializationDecl (_, _, _, _, _, _, _, {xrdi_is_pod}, _, _) -> | ClassTemplatePartialSpecializationDecl (_, _, _, _, _, _, _, {xrdi_is_pod}, _, _) )) ->
xrdi_is_pod xrdi_is_pod
| _ -> | _ ->
true ) true )

18
infer/src/concurrency/RacerDModels.ml
Unescape View File

@ -197,29 +197,29 @@ let is_cpp_container_write =
let is_container_write tenv pn = let is_container_write tenv pn =
match pn with match (pn : Procname.t) with
| Procname.CSharp _ when is_csharp_container_write tenv pn [] -> | CSharp _ when is_csharp_container_write tenv pn [] ->
true true
| Procname.Java _ when is_java_container_write tenv pn [] -> | Java _ when is_java_container_write tenv pn [] ->
true true
| (Procname.ObjC_Cpp _ | C _) when is_cpp_container_write pn -> | (ObjC_Cpp _ | C _) when is_cpp_container_write pn ->
true true
| _ -> | _ ->
false false
let is_container_read tenv pn = let is_container_read tenv pn =
match pn with match (pn : Procname.t) with
| Procname.CSharp _ -> | CSharp _ ->
is_csharp_container_read tenv pn [] is_csharp_container_read tenv pn []
| Procname.Java _ -> | Java _ ->
is_java_container_read tenv pn [] is_java_container_read tenv pn []
(* The following order matters: we want to check if pname is a container write (* The following order matters: we want to check if pname is a container write
before we check if pname is a container read. This is due to a different before we check if pname is a container read. This is due to a different
treatment between std::map::operator[] and all other operator[]. *) treatment between std::map::operator[] and all other operator[]. *)
| Procname.ObjC_Cpp _ | C _ -> | ObjC_Cpp _ | C _ ->
(not (is_cpp_container_write pn)) && is_cpp_container_read pn (not (is_cpp_container_write pn)) && is_cpp_container_read pn
| _ -> | Erlang _ | Linters_dummy_method | Block _ | WithBlockParameters _ ->
false false

2
infer/src/concurrency/starvationDomain.ml
Unescape View File

@ -132,7 +132,7 @@ module Lock = struct
the default depending on the language, since most Java locks are recursive and most C++ locks the default depending on the language, since most Java locks are recursive and most C++ locks
are not. *) are not. *)
match get_typ tenv lock with match get_typ tenv lock with
| Some {Typ.desc= Tptr ({desc= Tstruct name}, _)} | Some {desc= Tstruct name} -> | Some {Typ.desc= Tptr ({desc= Tstruct name}, _) | Tstruct name} ->
ConcurrencyModels.is_recursive_lock_type name ConcurrencyModels.is_recursive_lock_type name
| Some typ -> | Some typ ->
(* weird type passed as a lock, return default *) (* weird type passed as a lock, return default *)

2
infer/src/quandary/ClangTrace.ml
Unescape View File

@ -459,7 +459,7 @@ include TaintTrace.Make (struct
(not is_escaped) (not is_escaped)
&& &&
match typ with match typ with
| Some (Typ.Tint _ | Tfloat _ | Tvoid) -> | Some Typ.(Tint _ | Tfloat _ | Tvoid) ->
false false
| _ -> | _ ->
(* possible a string/object/struct type; assume injection possible *) (* possible a string/object/struct type; assume injection possible *)

12
infer/src/quandary/TaintAnalysis.ml
Unescape View File

@ -430,15 +430,13 @@ module Make (TaintSpecification : TaintSpec.S) = struct
existing machinery for adding function call sinks *) existing machinery for adding function call sinks *)
let add_sinks_for_access_path ({analysis_data= {tenv}} as analysis_data) access_expr loc astate let add_sinks_for_access_path ({analysis_data= {tenv}} as analysis_data) access_expr loc astate
= =
let rec add_sinks_for_access astate_acc = function let rec add_sinks_for_access astate_acc (access_expr : HilExp.AccessExpression.t) =
| HilExp.AccessExpression.Base _ -> match access_expr with
| Base _ ->
astate_acc astate_acc
| HilExp.AccessExpression.FieldOffset (ae, _) | FieldOffset (ae, _) | ArrayOffset (ae, _, None) | AddressOf ae | Dereference ae ->
| ArrayOffset (ae, _, None)
| AddressOf ae
| Dereference ae ->
add_sinks_for_access astate_acc ae add_sinks_for_access astate_acc ae
| HilExp.AccessExpression.ArrayOffset (ae, _, Some index) -> | ArrayOffset (ae, _, Some index) ->
let dummy_call_site = CallSite.make BuiltinDecl.__array_access loc in let dummy_call_site = CallSite.make BuiltinDecl.__array_access loc in
let dummy_actuals = let dummy_actuals =
List.map List.map

Write Preview
Loading…
Cancel
Save