diff --git a/infer/src/IR/AccessExpression.ml b/infer/src/IR/AccessExpression.ml index 95fae2ddb..b1c9633be 100644 --- a/infer/src/IR/AccessExpression.ml +++ b/infer/src/IR/AccessExpression.ml @@ -12,13 +12,70 @@ type typ_ = Typ.t let compare_typ_ _ _ = 0 -type t = - | Base of AccessPath.base - | FieldOffset of t * Typ.Fieldname.t - | ArrayOffset of t * typ_ * t list - | AddressOf of t - | Dereference of t -[@@deriving compare] +(** Module where unsafe construction of [t] is allowed. In the rest of the code, and especially in + clients of the whole [AccessExpression] module, we do not want to allow constructing access + expressions directly as they could introduce de-normalized expressions of the form [AddressOf + (Dereference t)] or [Dereference (AddressOf t)]. + + We could make only the types of [AddressOf] and [Dereference] private but that proved too + cumbersome... *) +module T : sig + type t = private + | Base of AccessPath.base + | FieldOffset of t * Typ.Fieldname.t + | ArrayOffset of t * Typ.t * t list + | AddressOf of t + | Dereference of t + [@@deriving compare] + + val base : AccessPath.base -> t + + val field_offset : t -> Typ.Fieldname.t -> t + + val array_offset : t -> Typ.t -> t list -> t + + val address_of : t -> t + + val dereference : t -> t + + val replace_base : remove_deref_after_base:bool -> AccessPath.base -> t -> t +end = struct + type t = + | Base of AccessPath.base + | FieldOffset of t * Typ.Fieldname.t + | ArrayOffset of t * typ_ * t list + | AddressOf of t + | Dereference of t + [@@deriving compare] + + let base base = Base base + + let field_offset t field = FieldOffset (t, field) + + let array_offset t typ elements = ArrayOffset (t, typ, elements) + + let address_of = function Dereference t -> t | t -> AddressOf t + + let dereference = function AddressOf t -> t | t -> Dereference t + + let rec replace_base ~remove_deref_after_base base_new access_expr = + let replace_base_inner = replace_base ~remove_deref_after_base base_new in + match access_expr with + | Dereference (Base _) -> + if remove_deref_after_base then Base base_new else Dereference (Base base_new) + | Base _ -> + Base base_new + | FieldOffset (ae, fld) -> + FieldOffset (replace_base_inner ae, fld) + | ArrayOffset (ae, typ, aes) -> + ArrayOffset (replace_base_inner ae, typ, aes) + | AddressOf ae -> + AddressOf (replace_base_inner ae) + | Dereference ae -> + Dereference (replace_base_inner ae) +end + +include T let may_pp_typ fmt typ = if Config.debug_level_analysis >= 3 then F.fprintf fmt ":%a" (Typ.pp Pp.text) typ @@ -44,11 +101,9 @@ let rec pp fmt = function module Access = struct - type access_expr = t [@@deriving compare] - - type t = + type nonrec t = | FieldAccess of Typ.Fieldname.t - | ArrayAccess of typ_ * access_expr list + | ArrayAccess of typ_ * t list | TakeAddress | Dereference [@@deriving compare] @@ -95,9 +150,7 @@ let rec to_access_path t = let access_paths = to_access_paths index_aes in let base, accesses = to_access_path_ ae in (base, AccessPath.ArrayAccess (typ, access_paths) :: accesses) - | AddressOf ae -> - to_access_path_ ae - | Dereference ae -> + | AddressOf ae | Dereference ae -> to_access_path_ ae in let base, accesses = to_access_path_ t in @@ -113,23 +166,6 @@ let rec get_base = function get_base ae -let rec replace_base ~remove_deref_after_base base_new access_expr = - let replace_base_inner = replace_base ~remove_deref_after_base base_new in - match access_expr with - | Dereference (Base _) -> - if remove_deref_after_base then Base base_new else Dereference (Base base_new) - | Base _ -> - Base base_new - | FieldOffset (ae, fld) -> - FieldOffset (replace_base_inner ae, fld) - | ArrayOffset (ae, typ, aes) -> - ArrayOffset (replace_base_inner ae, typ, aes) - | AddressOf ae -> - AddressOf (replace_base_inner ae) - | Dereference ae -> - Dereference (replace_base_inner ae) - - let is_base = function Base _ -> true | _ -> false let lookup_field_type_annot tenv base_typ field_name = @@ -164,32 +200,9 @@ let base_of_id id typ = (Var.of_id id, typ) let base_of_pvar pvar typ = (Var.of_pvar pvar, typ) -let of_pvar pvar typ = AddressOf (Base (base_of_pvar pvar typ)) - -let of_id id typ = Base (base_of_id id typ) - -(* cancel out consective *&'s *) -let rec normalize t = - match t with - | Base _ -> - t - | Dereference (AddressOf t1) -> - normalize t1 - | FieldOffset (t1, fieldname) -> - let t1' = normalize t1 in - if phys_equal t1 t1' then t else normalize (FieldOffset (t1', fieldname)) - | ArrayOffset (t1, typ, tlist) -> - let t1' = normalize t1 in - let tlist' = IList.map_changed ~f:normalize ~equal tlist in - if phys_equal t1 t1' && phys_equal tlist tlist' then t - else normalize (ArrayOffset (t1', typ, tlist')) - | Dereference t1 -> - let t1' = normalize t1 in - if phys_equal t1 t1' then t else normalize (Dereference t1') - | AddressOf t1 -> - let t1' = normalize t1 in - if phys_equal t1 t1' then t else normalize (AddressOf t1') +let of_pvar pvar typ = address_of (base (base_of_pvar pvar typ)) +let of_id id typ = base (base_of_id id typ) (* Adapted from AccessPath.of_exp. *) let of_exp ~include_array_indexes ~add_deref exp0 typ0 ~(f_resolve_id : Var.t -> t option) = @@ -198,11 +211,11 @@ let of_exp ~include_array_indexes ~add_deref exp0 typ0 ~(f_resolve_id : Var.t -> | Exp.Var id -> ( match f_resolve_id (Var.of_id id) with | Some access_expr -> - let access_expr' = if add_deref then Dereference access_expr else access_expr in + let access_expr' = if add_deref then dereference access_expr else access_expr in add_accesses access_expr' :: acc | None -> let access_expr = of_id id typ in - let access_expr' = if add_deref then Dereference access_expr else access_expr in + let access_expr' = if add_deref then dereference access_expr else access_expr in add_accesses access_expr' :: acc ) | Exp.Lvar pvar when Pvar.is_ssa_frontend_tmp pvar -> ( match f_resolve_id (Var.of_pvar pvar) with @@ -216,21 +229,21 @@ let of_exp ~include_array_indexes ~add_deref exp0 typ0 ~(f_resolve_id : Var.t -> add_accesses access_expr' :: acc | None -> let access_expr = of_pvar pvar typ in - let access_expr' = if add_deref then Dereference access_expr else access_expr in + let access_expr' = if add_deref then dereference access_expr else access_expr in add_accesses access_expr' :: acc ) | Exp.Lvar pvar -> let access_expr = of_pvar pvar typ in - let access_expr' = if add_deref then Dereference access_expr else access_expr in + let access_expr' = if add_deref then dereference access_expr else access_expr in add_accesses access_expr' :: acc | Exp.Lfield (root_exp, fld, root_exp_typ) -> - let add_field_access_expr access_expr = add_accesses (FieldOffset (access_expr, fld)) in + let add_field_access_expr access_expr = add_accesses (field_offset access_expr fld) in of_exp_ root_exp root_exp_typ add_field_access_expr acc | Exp.Lindex (root_exp, index_exp) -> let index_access_exprs = if include_array_indexes then of_exp_ index_exp typ Fn.id [] else [] in let add_array_access_expr access_expr = - add_accesses (ArrayOffset (access_expr, typ, index_access_exprs)) + add_accesses (array_offset access_expr typ index_access_exprs) in let array_typ = Typ.mk_array typ in of_exp_ root_exp array_typ add_array_access_expr acc @@ -245,14 +258,14 @@ let of_exp ~include_array_indexes ~add_deref exp0 typ0 ~(f_resolve_id : Var.t -> | Exp.Const _ | Closure _ | Sizeof _ -> acc in - IList.map_changed ~f:normalize ~equal (of_exp_ exp0 typ0 Fn.id []) + of_exp_ exp0 typ0 Fn.id [] let of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ ~(f_resolve_id : Var.t -> t option) = match lhs_exp with | Exp.Lfield _ when not add_deref -> ( let res = of_exp ~include_array_indexes ~add_deref:true lhs_exp typ ~f_resolve_id in - match res with [lhs_ae] -> Some (AddressOf lhs_ae) | _ -> None ) + match res with [lhs_ae] -> Some (address_of lhs_ae) | _ -> None ) | Exp.Lindex _ when not add_deref -> ( let res = let typ' = @@ -265,7 +278,7 @@ let of_lhs_exp ~include_array_indexes ~add_deref lhs_exp typ ~(f_resolve_id : Va in of_exp ~include_array_indexes ~add_deref:true lhs_exp typ' ~f_resolve_id in - match res with [lhs_ae] -> Some (AddressOf lhs_ae) | _ -> None ) + match res with [lhs_ae] -> Some (address_of lhs_ae) | _ -> None ) | _ -> ( let res = of_exp ~include_array_indexes ~add_deref lhs_exp typ ~f_resolve_id in match res with [lhs_ae] -> Some lhs_ae | _ -> None ) diff --git a/infer/src/IR/AccessExpression.mli b/infer/src/IR/AccessExpression.mli index 873161b8a..1bc6009b2 100644 --- a/infer/src/IR/AccessExpression.mli +++ b/infer/src/IR/AccessExpression.mli @@ -7,24 +7,31 @@ open! IStd -type t = +type t = private | Base of AccessPath.base - | FieldOffset of t * Typ.Fieldname.t - (* field access *) - | ArrayOffset of t * Typ.t * t list - (* array access *) - | AddressOf of t - (* address of operator & *) - | Dereference of t - (* dereference operator * *) + | FieldOffset of t * Typ.Fieldname.t (** field access *) + | ArrayOffset of t * Typ.t * t list (** array access *) + | AddressOf of t (** "address of" operator [&] *) + | Dereference of t (** "dereference" operator [*] *) [@@deriving compare] -module Access : sig - type access_expr = t [@@deriving compare] +val base : AccessPath.base -> t + +val field_offset : t -> Typ.Fieldname.t -> t + +val array_offset : t -> Typ.t -> t list -> t + +val address_of : t -> t + [@@warning "-32"] +(** guarantees that we never build [AddressOf (Dereference t)] expressions: these become [t] *) - type t = +val dereference : t -> t +(** guarantees that we never build [Dereference (AddressOf t)] expressions: these become [t] *) + +module Access : sig + type nonrec t = | FieldAccess of Typ.Fieldname.t - | ArrayAccess of Typ.t * access_expr list + | ArrayAccess of Typ.t * t list | TakeAddress | Dereference [@@deriving compare] @@ -61,5 +68,3 @@ val of_lhs_exp : -> f_resolve_id:(Var.t -> t option) -> t option (** convert [lhs_exp] to an access expression, resolving identifiers using [f_resolve_id] *) - -val normalize : t -> t diff --git a/infer/src/IR/HilExp.ml b/infer/src/IR/HilExp.ml index ff6a38d5f..0daa4bf5a 100644 --- a/infer/src/IR/HilExp.ml +++ b/infer/src/IR/HilExp.ml @@ -116,12 +116,10 @@ let of_sil ~include_array_indexes ~f_resolve_id ~add_deref exp typ = let ae = match f_resolve_id (Var.of_id id) with | Some access_expr -> - if add_deref then AccessExpression.normalize (Dereference access_expr) - else access_expr + if add_deref then AccessExpression.dereference access_expr else access_expr | None -> let access_expr = AccessExpression.of_id id typ in - if add_deref then AccessExpression.normalize (Dereference access_expr) - else access_expr + if add_deref then AccessExpression.dereference access_expr else access_expr in AccessExpression ae | UnOp (op, e, typ_opt) -> diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index dd30bc4f4..edd56d605 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -55,7 +55,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = | AccessExpression rhs_access_expr -> Bind (lhs_id, rhs_access_expr) | _ -> - Instr (Assign (AccessExpression.Base (lhs_id, rhs_typ), rhs_hil_exp, loc)) + Instr (Assign (AccessExpression.base (lhs_id, rhs_typ), rhs_hil_exp, loc)) in match instr with | Load (lhs_id, rhs_exp, rhs_typ, loc) -> @@ -98,7 +98,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = let dummy_base_var = Var.of_id (Ident.create_normal (Ident.string_to_name (IntLit.to_string i)) 0) in - AccessExpression.Base (dummy_base_var, Typ.void_star) + AccessExpression.base (dummy_base_var, Typ.void_star) | _ -> L.(die InternalError) "Non-assignable LHS expression %a at %a" Exp.pp lhs_exp Location.pp_file_pos loc diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 95a063068..2e9d2fada 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -69,7 +69,7 @@ struct let actual_state' = IdAccessPathMapDomain.fold (fun id access_expr astate_acc -> - let lhs_access_path = AccessExpression.Base (id, Typ.mk Typ.Tvoid) in + let lhs_access_path = AccessExpression.base (id, Typ.mk Typ.Tvoid) in let dummy_assign = HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc) in diff --git a/infer/src/checkers/Ownership.ml b/infer/src/checkers/Ownership.ml index cf4da8500..51f733c00 100644 --- a/infer/src/checkers/Ownership.ml +++ b/infer/src/checkers/Ownership.ml @@ -190,13 +190,13 @@ module Domain = struct (* handle assigning directly to a base var *) let handle_var_assign ?(is_operator_equal = false) lhs_base rhs_exp loc summary astate = - match rhs_exp with - | HilExp.Constant _ when not (Var.is_cpp_temporary (fst lhs_base)) -> + match (rhs_exp : HilExp.t) with + | Constant _ when not (Var.is_cpp_temporary (fst lhs_base)) -> add lhs_base CapabilityDomain.Owned astate - | HilExp.AccessExpression (Base rhs_base | AddressOf (Base rhs_base)) + | AccessExpression (Base rhs_base | AddressOf (Base rhs_base)) when not (Var.appears_in_source_code (fst rhs_base)) -> copy_or_borrow_var lhs_base rhs_base astate - | HilExp.Closure (_, captured_vars) -> + | Closure (_, captured_vars) -> (* TODO: can be folded into the case above once we have proper AccessExpressions *) let vars_captured_by_ref = List.fold captured_vars @@ -205,10 +205,10 @@ module Domain = struct ~init:VarSet.empty in borrow_vars lhs_base vars_captured_by_ref astate - | HilExp.AccessExpression (Base rhs_base) + | AccessExpression (Base rhs_base) when (not is_operator_equal) && Typ.is_reference (snd rhs_base) -> copy_or_borrow_var lhs_base rhs_base astate - | HilExp.AccessExpression (AddressOf (Base rhs_base)) when not is_operator_equal -> + | AccessExpression (AddressOf (Base rhs_base)) when not is_operator_equal -> borrow_vars lhs_base (VarSet.singleton rhs_base) astate | _ -> (* TODO: support capability transfer between source vars, other assignment modes *) diff --git a/infer/src/checkers/Pulse.ml b/infer/src/checkers/Pulse.ml index ffdb5ff1f..337ffda5b 100644 --- a/infer/src/checkers/Pulse.ml +++ b/infer/src/checkers/Pulse.ml @@ -49,9 +49,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Direct callee_pname when is_destructor callee_pname -> ( match actuals with | [AccessExpression destroyed_access] -> - let destroyed_object = - AccessExpression.normalize (AccessExpression.Dereference destroyed_access) - in + let destroyed_object = AccessExpression.dereference destroyed_access in PulseDomain.invalidate (CppDestructor (callee_pname, destroyed_object, call_loc)) call_loc destroyed_object astate @@ -60,9 +58,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> ( match actuals with | AccessExpression constructor_access :: rest -> - let constructed_object = - AccessExpression.normalize (AccessExpression.Dereference constructor_access) - in + let constructed_object = AccessExpression.dereference constructor_access in PulseDomain.havoc call_loc constructed_object astate >>= read_all rest | _ -> Ok astate ) diff --git a/infer/src/checkers/PulseDomain.ml b/infer/src/checkers/PulseDomain.ml index 324a1d5df..9c4293b9d 100644 --- a/infer/src/checkers/PulseDomain.ml +++ b/infer/src/checkers/PulseDomain.ml @@ -492,6 +492,11 @@ module Operations = struct walk actor ~on_last addr' path astate ) + let write_var var addr astate = + let stack = AliasingDomain.add var addr astate.stack in + {astate with stack} + + (** add addresses to the state to give a address to the destination of the given access path *) let walk_access_expr ~on_last astate access_expr location = let (access_var, _), access_list = AccessExpression.to_accesses access_expr in @@ -501,8 +506,7 @@ module Operations = struct access_list ; match (on_last, access_list) with | `Overwrite new_addr, [] -> - let stack = AliasingDomain.add access_var new_addr astate.stack in - Ok ({astate with stack}, new_addr) + Ok (write_var access_var new_addr astate, new_addr) | `Access, _ | `Overwrite _, _ :: _ -> let astate, base_addr = match AliasingDomain.find_opt access_var astate.stack with diff --git a/infer/src/checkers/PulseDomain.mli b/infer/src/checkers/PulseDomain.mli index 78a1cbd6a..e56b0e52c 100644 --- a/infer/src/checkers/PulseDomain.mli +++ b/infer/src/checkers/PulseDomain.mli @@ -43,6 +43,8 @@ val havoc_var : Var.t -> t -> t val havoc : Location.t -> AccessExpression.t -> t -> t access_result +val write_var : Var.t -> AbstractAddress.t -> t -> t + val write : Location.t -> AccessExpression.t -> AbstractAddress.t -> t -> t access_result val invalidate : PulseInvalidation.t -> Location.t -> AccessExpression.t -> t -> t access_result diff --git a/infer/src/checkers/PulseModels.ml b/infer/src/checkers/PulseModels.ml index 0196860dd..db6ad5d58 100644 --- a/infer/src/checkers/PulseModels.ml +++ b/infer/src/checkers/PulseModels.ml @@ -41,19 +41,19 @@ module Cplusplus = struct let placement_new : model = - fun location ~ret ~actuals astate -> + fun location ~ret:(ret_var, _) ~actuals astate -> match List.rev actuals with | HilExp.AccessExpression expr :: other_actuals -> let new_address = PulseDomain.AbstractAddress.mk_fresh () in PulseDomain.write location expr new_address astate - >>= PulseDomain.write location (Base ret) new_address + >>| PulseDomain.write_var ret_var new_address >>= PulseDomain.read_all location (List.concat_map other_actuals ~f:HilExp.get_access_exprs) | _ :: other_actuals -> PulseDomain.read_all location (List.concat_map other_actuals ~f:HilExp.get_access_exprs) astate - >>= PulseDomain.write location (Base ret) (PulseDomain.AbstractAddress.mk_fresh ()) + >>| PulseDomain.write_var ret_var (PulseDomain.AbstractAddress.mk_fresh ()) | _ -> Ok astate end @@ -66,10 +66,7 @@ module StdVector = struct let deref_internal_array vector = - AccessExpression.ArrayOffset - ( AccessExpression.Dereference (AccessExpression.FieldOffset (vector, internal_array)) - , Typ.void - , [] ) + AccessExpression.(array_offset (dereference (field_offset vector internal_array)) Typ.void []) let at : model = @@ -77,7 +74,7 @@ module StdVector = struct match actuals with | [AccessExpression vector; _index] -> PulseDomain.read location (deref_internal_array vector) astate - >>= fun (astate, loc) -> PulseDomain.write location (AccessExpression.Base ret) loc astate + >>= fun (astate, loc) -> PulseDomain.write location (AccessExpression.base ret) loc astate | _ -> Ok (PulseDomain.havoc_var (fst ret) astate) diff --git a/infer/src/checkers/purity.ml b/infer/src/checkers/purity.ml index 0dfb69103..b86fa53b5 100644 --- a/infer/src/checkers/purity.ml +++ b/infer/src/checkers/purity.ml @@ -27,12 +27,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = ProcData.no_extras let rec is_heap_access ae = - match ae with - | AccessExpression.FieldOffset _ | AccessExpression.ArrayOffset _ -> + match (ae : AccessExpression.t) with + | FieldOffset _ | ArrayOffset _ -> true - | AccessExpression.Dereference ae | AccessExpression.AddressOf ae -> + | Dereference ae | AddressOf ae -> is_heap_access ae - | AccessExpression.Base _ -> + | Base _ -> false diff --git a/infer/src/checkers/uninit.ml b/infer/src/checkers/uninit.ml index 3d07dc3a7..6b72e2976 100644 --- a/infer/src/checkers/uninit.ml +++ b/infer/src/checkers/uninit.ml @@ -282,7 +282,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | HilExp.Closure (_, apl) -> (* remove the captured variables of a block/lambda *) List.fold apl ~init:acc ~f:(fun acc (base, _) -> - MaybeUninitVars.remove (AccessExpression.Base base) acc ) + MaybeUninitVars.remove (AccessExpression.base base) acc ) | _ -> acc ) in @@ -308,7 +308,7 @@ module Initial = struct List.fold (Procdesc.get_locals pdesc) ~init:[] ~f:(fun acc (var_data : ProcAttributes.var_data) -> let pvar = Pvar.mk var_data.name (Procdesc.get_proc_name pdesc) in - let base_access_expr = AccessExpression.Base (Var.of_pvar pvar, var_data.typ) in + let base_access_expr = AccessExpression.base (Var.of_pvar pvar, var_data.typ) in match var_data.typ.Typ.desc with | Typ.Tstruct qual_name (* T30105165 remove filtering after we improve union translation *) @@ -318,7 +318,7 @@ module Initial = struct let flist = List.fold ~f:(fun acc' (fn, _, _) -> - AccessExpression.FieldOffset (base_access_expr, fn) :: acc' ) + AccessExpression.field_offset base_access_expr fn :: acc' ) ~init:acc fields in base_access_expr :: flist @@ -327,9 +327,9 @@ module Initial = struct | _ -> acc ) | Typ.Tarray {elt} -> - AccessExpression.ArrayOffset (base_access_expr, elt, []) :: acc + AccessExpression.array_offset base_access_expr elt [] :: acc | Typ.Tptr _ -> - base_access_expr :: AccessExpression.Dereference base_access_expr :: acc + base_access_expr :: AccessExpression.dereference base_access_expr :: acc | _ -> base_access_expr :: acc ) end diff --git a/infer/src/checkers/uninitDomain.ml b/infer/src/checkers/uninitDomain.ml index 6b2c539ed..f31de59eb 100644 --- a/infer/src/checkers/uninitDomain.ml +++ b/infer/src/checkers/uninitDomain.ml @@ -50,7 +50,7 @@ module MaybeUninitVars = struct match Tenv.lookup tenv name_struct with | Some {fields} -> List.fold fields ~init:maybe_uninit_vars ~f:(fun acc (fn, _, _) -> - remove (AccessExpression.FieldOffset (Base base, fn)) acc ) + remove (AccessExpression.field_offset (AccessExpression.base base) fn) acc ) | _ -> maybe_uninit_vars ) | _ -> @@ -60,7 +60,7 @@ module MaybeUninitVars = struct let remove_dereference_access base maybe_uninit_vars = match base with | _, {Typ.desc= Tptr _} -> - remove (AccessExpression.Dereference (Base base)) maybe_uninit_vars + remove (AccessExpression.dereference (AccessExpression.base base)) maybe_uninit_vars | _ -> maybe_uninit_vars @@ -68,7 +68,9 @@ module MaybeUninitVars = struct let remove_all_array_elements base maybe_uninit_vars = match base with | _, {Typ.desc= Tptr (elt, _)} -> - remove (AccessExpression.ArrayOffset (Base base, elt, [])) maybe_uninit_vars + remove + (AccessExpression.array_offset (AccessExpression.base base) elt []) + maybe_uninit_vars | _ -> maybe_uninit_vars diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 88f4a034d..606a55f64 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -455,8 +455,8 @@ module Make (TaintSpecification : TaintSpec.S) = struct astate_acc | AccessExpression.FieldOffset (ae, _) | ArrayOffset (ae, _, []) - | Dereference ae - | AddressOf ae -> + | AddressOf ae + | Dereference ae -> add_sinks_for_access astate_acc ae | AccessExpression.ArrayOffset (ae, _, indexes) -> let dummy_call_site = CallSite.make BuiltinDecl.__array_access loc in