diff --git a/facebook-clang-plugins b/facebook-clang-plugins index c7e476c39..84b3c58ab 160000 --- a/facebook-clang-plugins +++ b/facebook-clang-plugins @@ -1 +1 @@ -Subproject commit c7e476c39601eaf3ccaff272006c7da799cac208 +Subproject commit 84b3c58ab12fd42779ea4f8c1214432801cf4a5f diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index 4367231b6..44a5c17d1 100644 --- a/infer/src/IR/Typ.re +++ b/infer/src/IR/Typ.re @@ -105,10 +105,6 @@ let ptr_kind_string = | Pk_objc_unsafe_unretained => "__unsafe_unretained *" | Pk_objc_autoreleasing => "__autoreleasing *"; - -/** statically determined length of an array type, if any */ -type static_length = option IntLit.t [@@deriving compare]; - module T = { type type_quals = {is_const: bool, is_restrict: bool, is_volatile: bool} [@@deriving compare]; @@ -121,7 +117,7 @@ module T = { | Tfun bool /** function type with noreturn attribute */ | Tptr t ptr_kind /** pointer type */ | Tstruct name /** structured value type name */ - | Tarray t static_length /** array type with statically fixed length */ + | Tarray t (option IntLit.t) (option IntLit.t) /** array type with statically fixed length and stride */ [@@deriving compare] and name = | CStruct QualifiedCppName.t @@ -202,13 +198,13 @@ let rec pp_full pe f typ => { | Tptr ({desc: Tarray _ | Tfun _} as typ) pk => F.fprintf f "%a(%s)" (pp_full pe) typ (ptr_kind_string pk |> escape pe) | Tptr typ pk => F.fprintf f "%a%s" (pp_full pe) typ (ptr_kind_string pk |> escape pe) - | Tarray typ static_len => - let pp_array_static_len fmt => ( + | Tarray typ static_len static_stride => + let pp_int_opt fmt => ( fun - | Some static_len => IntLit.pp fmt static_len + | Some x => IntLit.pp fmt x | None => F.fprintf fmt "_" ); - F.fprintf f "%a[%a]" (pp_full pe) typ pp_array_static_len static_len + F.fprintf f "%a[%a*%a]" (pp_full pe) typ pp_int_opt static_len pp_int_opt static_stride }; F.fprintf f "%a%a" pp_desc typ pp_quals typ } @@ -393,7 +389,7 @@ let strip_ptr typ => If not, return the default type if given, otherwise raise an exception */ let array_elem default_opt typ => switch typ.desc { - | Tarray t_el _ => t_el + | Tarray t_el _ _ => t_el | _ => unsome "array_elem" default_opt }; @@ -411,7 +407,7 @@ let is_java_class = is_class_of_kind Name.Java.is_class; let rec is_array_of_cpp_class typ => switch typ.desc { - | Tarray typ _ => is_array_of_cpp_class typ + | Tarray typ _ _ => is_array_of_cpp_class typ | _ => is_cpp_class typ }; @@ -447,7 +443,7 @@ let rec java_from_string: string => t = | "double" => mk (Tfloat FDouble) | typ_str when String.contains typ_str '[' => { let stripped_typ = String.sub typ_str pos::0 len::(String.length typ_str - 2); - mk (Tptr (mk (Tarray (java_from_string stripped_typ) None)) Pk_pointer) + mk (Tptr (mk (Tarray (java_from_string stripped_typ) None None)) Pk_pointer) } | typ_str => mk (Tstruct (Name.Java.from_string typ_str)); @@ -1086,7 +1082,7 @@ module Struct = { /** the element typ of the final extensible array in the given typ, if any */ let rec get_extensible_array_element_typ ::lookup (typ: T.t) => switch typ.desc { - | Tarray typ _ => Some typ + | Tarray typ _ _ => Some typ | Tstruct name => switch (lookup name) { | Some {fields} => diff --git a/infer/src/IR/Typ.rei b/infer/src/IR/Typ.rei index 2b6b7d25c..0172bd9b5 100644 --- a/infer/src/IR/Typ.rei +++ b/infer/src/IR/Typ.rei @@ -65,10 +65,6 @@ type ptr_kind = let equal_ptr_kind: ptr_kind => ptr_kind => bool; - -/** statically determined length of an array type, if any */ -type static_length = option IntLit.t [@@deriving compare]; - type type_quals [@@deriving compare]; let mk_type_quals: @@ -86,8 +82,6 @@ let is_restrict: type_quals => bool; let is_volatile: type_quals => bool; -/** types for sil (structured) expressions */ - /** types for sil (structured) expressions */ type t = {desc, quals: type_quals} [@@deriving compare] and desc = @@ -97,7 +91,7 @@ and desc = | Tfun bool /** function type with noreturn attribute */ | Tptr t ptr_kind /** pointer type */ | Tstruct name /** structured value type name */ - | Tarray t static_length /** array type with statically fixed length */ + | Tarray t (option IntLit.t) (option IntLit.t) /** array type with statically fixed stride and length */ [@@deriving compare] and name = | CStruct QualifiedCppName.t diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index 5f6418060..a994bbfaf 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -47,7 +47,7 @@ let extract_array_type typ = else match typ.Typ.desc with | Typ.Tarray _ -> Some typ - | Typ.Tptr (elt, _) -> Some (Typ.mk ~default:typ (Tarray (elt, None))) + | Typ.Tptr (elt, _) -> Some (Typ.mk ~default:typ (Tarray (elt, None, None))) | _ -> None (** Return a result from a procedure call. *) @@ -753,10 +753,10 @@ let execute_alloc mk can_return_null Exp.BinOp (bop, evaluate_char_sizeof e1', evaluate_char_sizeof e2') | Exp.Exn _ | Exp.Closure _ | Exp.Const _ | Exp.Cast _ | Exp.Lvar _ | Exp.Lfield _ | Exp.Lindex _ -> e - | Exp.Sizeof {typ={Typ.desc=Tarray ({Typ.desc=Tint ik}, _)}; dynamic_length=Some len} + | Exp.Sizeof {typ={Typ.desc=Tarray ({Typ.desc=Tint ik}, _, _)}; dynamic_length=Some len} when Typ.ikind_is_char ik -> evaluate_char_sizeof len - | Exp.Sizeof {typ={Typ.desc=Tarray ({Typ.desc=Tint ik}, Some len)}; dynamic_length=None} + | Exp.Sizeof {typ={Typ.desc=Tarray ({Typ.desc=Tint ik}, Some len, _)}; dynamic_length=None} when Typ.ikind_is_char ik -> evaluate_char_sizeof (Exp.Const (Const.Cint len)) | Exp.Sizeof _ -> e in @@ -780,7 +780,7 @@ let execute_alloc mk can_return_null let n_size_exp' = evaluate_char_sizeof n_size_exp in Prop.exp_normalize_prop tenv prop n_size_exp', prop in let cnt_te = - Exp.Sizeof {typ=Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), None)); + Exp.Sizeof {typ=Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), None, Some (IntLit.of_int 1))); nbytes=None; dynamic_length=Some size_exp'; subtype=Subtype.exact} in let id_new = Ident.create_fresh Ident.kprimed in let exp_new = Exp.Var id_new in diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index 5213fd273..044ca874e 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -84,7 +84,7 @@ end = struct | None -> fail () ) - | Sil.Earray (_, esel, _), Typ.Tarray (t', _), Index ind :: syn_offs' -> + | Sil.Earray (_, esel, _), Typ.Tarray (t', _, _), Index ind :: syn_offs' -> let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' ind) esel) in get_strexp_at_syn_offsets tenv se' t' syn_offs' | _ -> @@ -111,7 +111,7 @@ end = struct | None -> assert false ) - | Sil.Earray (len, esel, inst), Tarray (t', _), Index idx :: syn_offs' -> + | Sil.Earray (len, esel, inst), Tarray (t', _, _), Index idx :: syn_offs' -> let se' = snd (List.find_exn ~f:(fun (i', _) -> Exp.equal i' idx) esel) in let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in let esel' = @@ -171,7 +171,7 @@ end = struct | None -> () ) - | Sil.Earray (_, esel, _), Tarray (t, _) -> + | Sil.Earray (_, esel, _), Tarray (t, _, _) -> find_offset_esel sigma_other hpred root offs esel t | _ -> () end @@ -443,7 +443,7 @@ let keep_only_indices tenv (** If the type is array, check whether we should do abstraction *) let array_typ_can_abstract {Typ.desc} = match desc with - | Tarray ({desc=Tptr ({desc=Tfun _}, _)}, _) -> false (* don't abstract arrays of pointers *) + | Tarray ({desc=Tptr ({desc=Tfun _}, _)}, _, _) -> false (* don't abstract arrays of pointers *) | _ -> true (** This function checks whether we can apply an abstraction to a strexp *) diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 84397b604..b2d4118dd 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -1006,10 +1006,12 @@ and typ_partial_join (t1 : Typ.t) (t2 : Typ.t) = match t1.desc, t2.desc with | Typ.Tptr (t1, pk1), Typ.Tptr (t2, pk2) when Typ.equal_ptr_kind pk1 pk2 && Typ.equal_quals t1.quals t2.quals -> Typ.mk ~default:t1 (Tptr (typ_partial_join t1 t2, pk1)) (* quals are the same for t1 and t2 *) - | Typ.Tarray (typ1, len1), Typ.Tarray (typ2, len2) when Typ.equal_quals typ1.quals typ2.quals -> + | Typ.Tarray (typ1, len1, stride1), + Typ.Tarray (typ2, len2, stride2) when Typ.equal_quals typ1.quals typ2.quals -> let t = typ_partial_join typ1 typ2 in let len = static_length_partial_join len1 len2 in - Typ.mk ~default:t1 (Tarray (t, len)) (* quals are the same for t1 and t2 *) + let stride = static_length_partial_join stride1 stride2 in + Typ.mk ~default:t1 (Tarray (t, len, stride)) (* quals are the same for t1 and t2 *) | _ when Typ.equal t1 t2 -> t1 (* common case *) | _ -> L.d_str "typ_partial_join no match "; diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 54a620cac..01fd5c19d 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -298,7 +298,7 @@ let rec dotty_mk_node pe sigma = let n = !dotty_state_count in incr dotty_state_count; let do_hpred_lambda exp_color = function - | (Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof {typ={Typ.desc=Tarray (t, _)}}), + | (Sil.Hpointsto (e, Sil.Earray (e', l, _), Exp.Sizeof {typ={Typ.desc=Tarray (t, _, _)}}), lambda) -> incr dotty_state_count; (* increment once more n+1 is the box for the array *) let e_color_str = color_to_str (exp_color e) in diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 2d0a99494..ee8e8b446 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -489,7 +489,7 @@ let rec create_strexp_of_type tenv struct_init_mode (typ : Typ.t) len inst : Sil | _ -> Estruct ([], inst) ) - | Tarray (_, len_opt), None -> + | Tarray (_, len_opt, _), None -> let len = match len_opt with | None -> Exp.get_undefined false | Some len -> Exp.Const (Cint len) in @@ -548,7 +548,7 @@ let exp_collapse_consecutive_indices_prop (typ : Typ.t) exp = false in let typ_is_one_step_from_base = match typ.desc with - | Tptr (t, _) | Tarray (t, _) -> + | Tptr (t, _) | Tarray (t, _, _) -> typ_is_base t | _ -> false in @@ -712,10 +712,10 @@ module Normalize = struct Closure { c with captured_vars; } | Const _ -> e - | Sizeof {typ={desc=Tarray ({desc=Tint ik}, _)}; dynamic_length=Some l} + | Sizeof {typ={desc=Tarray ({desc=Tint ik}, _, _)}; dynamic_length=Some l} when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang -> eval l - | Sizeof {typ={desc=Tarray ({desc=Tint ik}, Some l)}} + | Sizeof {typ={desc=Tarray ({desc=Tint ik}, Some l, _)}} when Typ.ikind_is_char ik && Config.curr_language_is Config.Clang -> Const (Cint l) | Sizeof _ -> @@ -991,12 +991,12 @@ module Normalize = struct Exp.int (IntLit.div n m) | Const (Cfloat v), Const (Cfloat w) -> Exp.float (v /.w) - | Sizeof {typ={desc=Tarray (elt, _)}; dynamic_length=Some len}, + | Sizeof {typ={desc=Tarray (elt, _, _)}; dynamic_length=Some len}, Sizeof {typ=elt2; dynamic_length=None} (* pattern: sizeof(elt[len]) / sizeof(elt) = len *) when Typ.equal elt elt2 -> len - | Sizeof {typ={desc=Tarray (elt, Some len)}; dynamic_length=None}, + | Sizeof {typ={desc=Tarray (elt, Some len, _)}; dynamic_length=None}, Sizeof {typ=elt2; dynamic_length=None} (* pattern: sizeof(elt[len]) / sizeof(elt) = len *) when Typ.equal elt elt2 -> @@ -1381,27 +1381,27 @@ module Normalize = struct let hpred' = mk_ptsto_exp tenv Fld_init (root, size, None) inst in replace_hpred hpred' | Earray (BinOp (Mult, Sizeof {typ=t; dynamic_length=None; subtype=st1}, x), esel, inst), - Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal t elt -> + Sizeof {typ={desc=Tarray (elt, _, _)} as arr} when Typ.equal t elt -> let dynamic_length = Some x in let sizeof_data = {Exp.typ=arr; nbytes=None; dynamic_length; subtype=st1} in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in replace_hpred (replace_array_contents hpred' esel) | Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length=None; subtype}), esel, inst), - Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal typ elt -> + Sizeof {typ={desc=Tarray (elt, _, _)} as arr} when Typ.equal typ elt -> let sizeof_data = {Exp.typ=arr; nbytes=None; dynamic_length=Some x; subtype} in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in replace_hpred (replace_array_contents hpred' esel) | Earray (BinOp (Mult, Sizeof {typ; dynamic_length=Some len; subtype}, x), esel, inst), - Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal typ elt -> + Sizeof {typ={desc=Tarray (elt, _, _)} as arr} when Typ.equal typ elt -> let sizeof_data = {Exp.typ=arr; nbytes=None; dynamic_length=Some (Exp.BinOp(Mult, x, len)); subtype} in let hpred' = mk_ptsto_exp tenv Fld_init (root, Sizeof sizeof_data, None) inst in replace_hpred (replace_array_contents hpred' esel) | Earray (BinOp (Mult, x, Sizeof {typ; dynamic_length=Some len; subtype}), esel, inst), - Sizeof {typ={desc=Tarray (elt, _)} as arr} when Typ.equal typ elt -> + Sizeof {typ={desc=Tarray (elt, _, _)} as arr} when Typ.equal typ elt -> let sizeof_data = {Exp.typ=arr; nbytes=None; dynamic_length=Some (Exp.BinOp(Mult, x, len)); subtype} in let hpred' = diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 6cb8e8c72..30d85515d 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -39,7 +39,7 @@ let rec remove_redundancy have_same_key acc = function let rec is_java_class tenv (typ: Typ.t) = match typ.desc with | Tstruct name -> Typ.Name.Java.is_class name - | Tarray (inner_typ, _) | Tptr (inner_typ, _) -> is_java_class tenv inner_typ + | Tarray (inner_typ, _, _) | Tptr (inner_typ, _) -> is_java_class tenv inner_typ | _ -> false (** Negate an atom *) @@ -400,7 +400,7 @@ end = struct List.iter ~f:(fun (f, se) -> strexp_extract (se, get_field_type f)) fsel | Sil.Earray (len, isel, _), t -> let elt_t = match t with - | Some {Typ.desc=Tarray (t, _)} -> Some t + | Some {Typ.desc=Tarray (t, _, _)} -> Some t | _ -> None in add_lt_minus1_e len; List.iter ~f:(fun (idx, se) -> @@ -1343,7 +1343,7 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 : sexp_imply tenv source calc_index_frame calc_missing subs se1' se2 typ2 | Sil.Earray (len, _, _), Sil.Eexp (_, inst) -> let se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in - let typ2' = Typ.mk (Tarray (typ2, None)) in + let typ2' = Typ.mk (Tarray (typ2, None, None)) in (* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2 argument is only used by eventually passing its value to Typ.Struct.fld, Exp.Lfield, Typ.Struct.fld, or Typ.array_elem. None of these are sensitive to the length field @@ -1533,7 +1533,7 @@ let expand_hpred_pointer = | Sil.Hpointsto (Exp.Lindex (e, ind), se, t) -> let t' = match t with | Exp.Sizeof ({typ=t_} as sizeof_data) -> - Exp.Sizeof {sizeof_data with typ=Typ.mk (Tarray (t_, None))} + Exp.Sizeof {sizeof_data with typ=Typ.mk (Tarray (t_, None, None))} | _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in let len = match t' with | Exp.Sizeof {dynamic_length=Some len} -> len @@ -1566,7 +1566,7 @@ struct match t1.Typ.desc, t2.Typ.desc with | Tstruct (JavaClass _ as cn1), Tstruct (JavaClass _ as cn2) -> Subtype.is_known_subtype tenv cn1 cn2 - | Tarray (dom_type1, _), Tarray (dom_type2, _) -> + | Tarray (dom_type1, _, _), Tarray (dom_type2, _, _) -> check_subtype_java tenv dom_type1 dom_type2 | Tptr (dom_type1, _), Tptr (dom_type2, _) -> check_subtype_java tenv dom_type1 dom_type2 @@ -1603,7 +1603,7 @@ struct (* and the algorithm will only work correctly if this is the case *) when Subtype.is_known_subtype tenv cn1 cn2 || Subtype.is_known_subtype tenv cn2 cn1 -> Subtype.case_analysis tenv (cn1, st1) (cn2, st2) - | Tarray (dom_type1, _), Tarray (dom_type2, _) -> + | Tarray (dom_type1, _, _), Tarray (dom_type2, _, _) -> case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) | Tptr (dom_type1, _), Tptr (dom_type2, _) -> case_analysis_type tenv (dom_type1, st1) (dom_type2, st2) @@ -2000,7 +2000,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 * let const_string_texp = match !Config.curr_language with | Config.Clang -> - Exp.Sizeof {typ=Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), Some len)); + Exp.Sizeof {typ=Typ.mk (Tarray (Typ.mk (Tint Typ.IChar), + Some len, Some (IntLit.of_int 1))); nbytes=None; dynamic_length=None; subtype=Subtype.exact} | Config.Java -> let object_type = Typ.Name.Java.from_string "java.lang.String" in diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 7ef582505..d886d5b6b 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -133,9 +133,9 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp let e' = Sil.array_clean_new_index footprint_part e in let len = Exp.Var (new_id ()) in let se = Sil.Earray (len, [(e', se')], inst) in - let res_t = Typ.mk (Tarray (res_t', None)) in + let res_t = Typ.mk (Tarray (res_t', None, None)) in (Sil.Aeq (e, e') :: atoms', se, res_t) - | Tarray (t', len_), off -> + | Tarray (t', len_, stride_), off -> let len = match len_ with | None -> Exp.Var (new_id ()) | Some len -> Exp.Const (Const.Cint len) in @@ -149,7 +149,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp pname tenv orig_prop footprint_part kind max_stamp t' off' inst in let e' = Sil.array_clean_new_index footprint_part e in let se = Sil.Earray (len, [(e', se')], inst) in - let res_t = Typ.mk ~default:t (Tarray (res_t', len_)) in + let res_t = Typ.mk ~default:t (Tarray (res_t', len_, stride_)) in (Sil.Aeq(e, e') :: atoms', se, res_t) | (Sil.Off_fld _) :: _ -> assert false @@ -168,7 +168,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp pname tenv orig_prop footprint_part kind max_stamp t' off' inst in let e' = Sil.array_clean_new_index footprint_part e in let se = Sil.Earray (len, [(e', se')], inst) in - let res_t = mk_typ_f (Tarray (res_t', None)) in + let res_t = mk_typ_f (Tarray (res_t', None, None)) in (Sil.Aeq(e, e') :: atoms', se, res_t) | Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ -> fail t off __POS__ @@ -261,10 +261,12 @@ let rec _strexp_extend_values if Config.type_size then Exp.one (* Exp.Sizeof (typ, Subtype.exact) *) else Exp.Var (new_id ()) in let se_new = Sil.Earray (len, [(Exp.zero, se)], inst) in - let typ_new = Typ.mk (Tarray (typ, None)) in + let typ_new = Typ.mk (Tarray (typ, None, None)) in _strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst - | (Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Tarray (typ', len_for_typ') -> ( + | (Off_index e) :: off', + Sil.Earray (len, esel, inst_arr), + Tarray (typ', len_for_typ', stride) -> ( bounds_check tenv pname orig_prop len e (State.get_loc ()); match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with | Some (_, se') -> @@ -277,7 +279,7 @@ let rec _strexp_extend_values if (Typ.equal res_typ' typ') || Int.equal (List.length res_esel') 1 then ( res_atoms' , Sil.Earray (len, res_esel', inst_arr) - , Typ.mk ~default:typ (Tarray (res_typ', len_for_typ')) ) + , Typ.mk ~default:typ (Tarray (res_typ', len_for_typ', stride)) ) :: acc else raise (Exceptions.Bad_footprint __POS__) in @@ -310,7 +312,7 @@ and array_case_analysis_index pname tenv orig_prop if index_in_array then let array_default = Sil.Earray (array_len, array_cont, inst_arr) in - let typ_default = Typ.mk ~default:typ_array (Tarray (typ_cont, typ_array_len)) in + let typ_default = Typ.mk ~default:typ_array (Tarray (typ_cont, typ_array_len, None)) in [([], array_default, typ_default)] else if !Config.footprint then begin let atoms, elem_se, elem_typ = @@ -319,7 +321,7 @@ and array_case_analysis_index pname tenv orig_prop check_sound elem_typ; let cont_new = List.sort ~cmp:[%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in let array_new = Sil.Earray (array_len, cont_new, inst_arr) in - let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len)) in + let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len, None)) in [(atoms, array_new, typ_new)] end else begin @@ -333,7 +335,7 @@ and array_case_analysis_index pname tenv orig_prop let cont_new = List.sort ~cmp:[%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in let array_new = Sil.Earray (array_len, cont_new, inst_arr) in - let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len)) in + let typ_new = Typ.mk ~default:typ_array (Tarray (elem_typ, typ_array_len, None)) in [(atoms, array_new, typ_new)] end in let rec handle_case acc isel_seen_rev = function @@ -349,7 +351,7 @@ and array_case_analysis_index pname tenv orig_prop let atoms_new = Sil.Aeq (index, i) :: atoms' in let isel_new = list_rev_and_concat isel_seen_rev ((i, se'):: isel_unseen) in let array_new = Sil.Earray (array_len, isel_new, inst_arr) in - let typ_new = Typ.mk ~default:typ_array (Tarray (typ', typ_array_len)) in + let typ_new = Typ.mk ~default:typ_array (Tarray (typ', typ_array_len, None)) in (atoms_new, array_new, typ_new):: acc') ~init:[] atoms_se_typ_list in @@ -1146,7 +1148,7 @@ let type_at_offset tenv texp off = | None -> None ) - | (Off_index _) :: off', Tarray (typ', _) -> + | (Off_index _) :: off', Tarray (typ', _, _) -> strip_offset off' typ' | _ -> None in match texp with @@ -1204,7 +1206,7 @@ let rec iter_rearrange typ_from_instr ) | Sil.Off_index _ :: off -> - Typ.mk (Tarray (root_typ_of_offsets off, None)) + Typ.mk (Tarray (root_typ_of_offsets off, None, None)) | _ -> typ_from_instr in let typ = root_typ_of_offsets (Sil.exp_get_offsets lexp) in diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 5ad930af9..5a56b82ff 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -37,7 +37,7 @@ let unroll_type tenv (typ: Typ.t) (off: Sil.offset) = | None -> fail Fieldname.to_string fld ) - | Tarray (typ', _), Off_index _ -> + | Tarray (typ', _, _), Off_index _ -> typ' | _, Off_index (Const (Cint i)) when IntLit.iszero i -> typ @@ -170,7 +170,9 @@ let rec apply_offlist pp_error(); assert false - | (Sil.Off_index idx) :: offlist', Sil.Earray (len, esel, inst1), Typ.Tarray (t', len') -> ( + | (Sil.Off_index idx) :: offlist', + Sil.Earray (len, esel, inst1), + Typ.Tarray (t', len', stride') -> ( let nidx = Prop.exp_normalize_prop tenv p idx in match List.find ~f:(fun ese -> Prover.check_equal tenv p nidx (fst ese)) esel with | Some (idx_ese', se') -> @@ -183,7 +185,7 @@ let rec apply_offlist then (idx_ese', res_se') else ese in let res_se = Sil.Earray (len, List.map ~f:replace_ese esel, inst1) in - let res_t = Typ.mk ~default:typ (Tarray (res_t', len')) in + let res_t = Typ.mk ~default:typ (Tarray (res_t', len', stride')) in (res_e', res_se, res_t, res_pred_insts_op') | None -> (* return a nondeterministic value if the index is not found after rearrangement *) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 1dea1ca8e..2c7b625e2 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -162,7 +162,7 @@ let diff : astate -> astate -> Itv.t let diff_join k a2 acc = match find k arr1 with | a1 -> Itv.join acc (ArrInfo.diff a1 a2) - | exception Not_found -> acc + | exception Not_found -> Itv.top in fold diff_join arr2 Itv.bot diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index fa3ffdcad..a5a4b1bc0 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -109,12 +109,12 @@ struct | _ -> model_unknown_itv ret mem let rec declare_array - : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> IntLit.t -> inst_num:int - -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate - = fun pname node loc typ len ~inst_num ~dimension mem -> - let size = IntLit.to_int len |> Itv.of_int in + : Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> length:IntLit.t -> ?stride:int + -> inst_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate + = fun pname node loc typ ~length ?stride ~inst_num ~dimension mem -> + let size = IntLit.to_int length |> Itv.of_int in let arr = - Sem.eval_array_alloc pname node typ Itv.zero size inst_num dimension + Sem.eval_array_alloc pname node typ Itv.zero size ?stride inst_num dimension in let mem = if Int.equal dimension 1 @@ -125,9 +125,9 @@ struct Loc.of_allocsite (Sem.get_allocsite pname node inst_num dimension) in match typ.Typ.desc with - | Typ.Tarray (typ, Some len) -> - declare_array pname node loc typ len ~inst_num - ~dimension:(dimension + 1) mem + | Typ.Tarray (typ, Some length, stride) -> + declare_array pname node loc typ ~length ?stride:(Option.map ~f:IntLit.to_int stride) + ~inst_num ~dimension:(dimension + 1) mem | _ -> mem let declare_symbolic_array @@ -236,10 +236,11 @@ struct let pname = Procdesc.get_proc_name pdesc in let try_decl_arr (mem, inst_num) (pvar, typ) = match typ.Typ.desc with - | Typ.Tarray (typ, Some len) -> + | Typ.Tarray (typ, Some length, stride0) -> let loc = Loc.of_pvar pvar in + let stride = Option.map ~f:IntLit.to_int stride0 in let mem = - declare_array pname node loc typ len ~inst_num ~dimension:1 mem + declare_array pname node loc typ ~length ?stride ~inst_num ~dimension:1 mem in (mem, inst_num + 1) | _ -> (mem, inst_num) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 80b1547e6..1dbe39503 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -50,7 +50,8 @@ struct | Typ.Tvoid -> 1 | Typ.Tptr (_, _) -> 4 | Typ.Tstruct _ -> 4 (* TODO *) - | Typ.Tarray (typ, Some ilit) -> sizeof typ * IntLit.to_int ilit + | Typ.Tarray (_, Some length, Some stride) -> IntLit.to_int stride * IntLit.to_int length + | Typ.Tarray (typ, Some length, None) -> sizeof typ * IntLit.to_int length | _ -> 4 let rec must_alias : Exp.t -> Exp.t -> Mem.astate -> bool diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 5d286d165..b839fe6b2 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -112,7 +112,7 @@ let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> Raw.t option) = of_exp_ root_exp root_exp_typ (field_access :: accesses) acc | Exp.Lindex (root_exp, _) -> let array_access = ArrayAccess typ in - let array_typ = Typ.mk (Tarray (typ, None)) in + let array_typ = Typ.mk (Tarray (typ, None, None)) in of_exp_ root_exp array_typ (array_access :: accesses) acc | Exp.Cast (cast_typ, cast_exp) -> of_exp_ cast_exp cast_typ [] acc diff --git a/infer/src/clang/ast_expressions.ml b/infer/src/clang/ast_expressions.ml index 0e7883145..a6062a08b 100644 --- a/infer/src/clang/ast_expressions.ml +++ b/infer/src/clang/ast_expressions.ml @@ -405,7 +405,8 @@ let translate_block_enumerate block_name stmt_info stmt_list ei = let parameter = Clang_ast_t.UnaryExprOrTypeTraitExpr ((fresh_stmt_info stmt_info), [], make_general_expr_info create_unsigned_long_type `RValue `Ordinary, - { Clang_ast_t.uttei_kind = `SizeOf 1; Clang_ast_t.uttei_qual_type = type_opt}) in + {Clang_ast_t.uttei_kind = `SizeOfWithSize 1; + Clang_ast_t.uttei_qual_type = type_opt}) in let pointer = di.Clang_ast_t.di_pointer in let stmt_info = fresh_stmt_info stmt_info in let malloc_name = CAst_utils.make_name_decl CFrontend_config.malloc in diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 1f00e0c89..049860b2b 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -415,7 +415,8 @@ struct let tenv = trans_state.context.CContext.tenv in let typ = CType_decl.qual_type_to_sil_type tenv expr_info.Clang_ast_t.ei_qual_type in match unary_expr_or_type_trait_expr_info.Clang_ast_t.uttei_kind with - | `SizeOf nbytes0 -> + | `SizeOf + | `SizeOfWithSize _ as size -> let qt_opt = CAst_utils.type_from_unary_expr_or_type_trait_expr_info unary_expr_or_type_trait_expr_info in @@ -423,11 +424,9 @@ struct match qt_opt with | Some qt -> CType_decl.qual_type_to_sil_type tenv qt | None -> typ (* Some default type since the type is missing *) in - let nbytes = if nbytes0 < 0 then - (* nbytes < 0 when the sizeof cannot be statically determined *) - None - else - Some nbytes0 in + let nbytes = match size with + | `SizeOfWithSize nbytes -> Some nbytes + | _ -> None in let sizeof_data = {Exp.typ=sizeof_typ; nbytes; dynamic_length=None; subtype=Subtype.exact} in { empty_res_trans with exps = [(Exp.Sizeof sizeof_data, sizeof_typ)] } @@ -2077,7 +2076,7 @@ struct and initListExpr_initializers_trans trans_state var_exp n stmts typ is_dyn_array stmt_info = let (var_exp_inside, typ_inside) = match typ.Typ.desc with - | Typ.Tarray (t, _) when Typ.is_array_of_cpp_class typ -> + | Typ.Tarray (t, _, _) when Typ.is_array_of_cpp_class typ -> Exp.Lindex (var_exp, Exp.Const (Const.Cint (IntLit.of_int n))), t | _ when is_dyn_array -> Exp.Lindex (var_exp, Exp.Const (Const.Cint (IntLit.of_int n))), typ diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 4b03de352..35d3a3c3d 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -727,7 +727,7 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero = | None -> assert false ) - | Tarray (arrtyp, Some n) -> + | Tarray (arrtyp, Some n, _) -> let size = IntLit.to_int n in let indices = list_range 0 (size - 1) in let index_constants = diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml index 536a19516..c16398721 100644 --- a/infer/src/clang/cType_to_sil_type.ml +++ b/infer/src/clang/cType_to_sil_type.ml @@ -59,10 +59,12 @@ let pointer_attribute_of_objc_attribute attr_info = | `OCL_Weak -> Typ.Pk_objc_weak | `OCL_Autoreleasing -> Typ.Pk_objc_autoreleasing -let rec build_array_type translate_decl tenv (qual_type : Clang_ast_t.qual_type) n_opt = +let rec build_array_type translate_decl tenv (qual_type : Clang_ast_t.qual_type) + length_opt stride_opt = let array_type = qual_type_to_sil_type translate_decl tenv qual_type in - let len = Option.map ~f:(fun n -> IntLit.of_int64 (Int64.of_int n)) n_opt in - Typ.Tarray (array_type, len) + let length = Option.map ~f:IntLit.of_int length_opt in + let stride = Option.map ~f:IntLit.of_int stride_opt in + Typ.Tarray (array_type, length, stride) and type_desc_of_attr_type translate_decl tenv type_info attr_info = match type_info.Clang_ast_t.ti_desugared_type with @@ -92,12 +94,13 @@ and type_desc_of_c_type translate_decl tenv c_type : Typ.desc = | BlockPointerType (_, qual_type) -> let typ = qual_type_to_sil_type translate_decl tenv qual_type in Typ.Tptr (typ, Typ.Pk_pointer) - | IncompleteArrayType (_, qual_type) - | DependentSizedArrayType (_, qual_type) - | VariableArrayType (_, qual_type) -> - build_array_type translate_decl tenv qual_type None - | ConstantArrayType (_, qual_type, n) -> - build_array_type translate_decl tenv qual_type (Some n) + | IncompleteArrayType (_, {arti_element_type; arti_stride}) + | DependentSizedArrayType (_, {arti_element_type; arti_stride}) -> + build_array_type translate_decl tenv arti_element_type None arti_stride + | VariableArrayType (_, {arti_element_type; arti_stride}) -> + build_array_type translate_decl tenv arti_element_type None arti_stride + | ConstantArrayType (_, {arti_element_type; arti_stride}, n) -> + build_array_type translate_decl tenv arti_element_type (Some n) arti_stride | FunctionProtoType _ | FunctionNoProtoType _ -> Typ.Tfun false diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index fdbf25eb6..483e038bd 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -85,9 +85,9 @@ let rec inhabit_typ tenv typ cfg env = try (TypMap.find typ env.cache, env) with Not_found -> let inhabit_internal typ env = match typ.Typ.desc with - | Typ.Tptr ({desc=Tarray (inner_typ, Some _)}, Typ.Pk_pointer) -> + | Typ.Tptr ({desc=Tarray (inner_typ, Some _, _)}, Typ.Pk_pointer) -> let len = Exp.Const (Const.Cint (IntLit.one)) in - let arr_typ = Typ.mk (Tarray (inner_typ, Some IntLit.one)) in + let arr_typ = Typ.mk (Tarray (inner_typ, Some IntLit.one, None)) in inhabit_alloc arr_typ (Some len) typ BuiltinDecl.__new_array env | Typ.Tptr (typ, Typ.Pk_pointer) -> (* TODO (t4575417): this case does not work correctly for enums, but they are currently diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index d6066b4dd..e9a2067cc 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -469,7 +469,7 @@ let rec expression (context : JContext.t) pc expr = match binop with | JBir.ArrayLoad _ -> (* add an instruction that dereferences the array *) - let array_typ = Typ.mk (Tarray (type_of_expr, None)) in + let array_typ = Typ.mk (Tarray (type_of_expr, None, None)) in let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in let id = Ident.create_fresh Ident.knormal in let load_instr = @@ -623,7 +623,7 @@ let get_array_length context pc expr_list content_type = (instrs @ other_instrs, sil_len_expr :: other_exprs) in let (instrs, sil_len_exprs) = List.fold_right ~f:get_expr_instr expr_list ~init:([],[]) in let get_array_type_len sil_len_expr (content_type, _) = - (Typ.mk (Tarray (content_type, None)), Some sil_len_expr) in + (Typ.mk (Tarray (content_type, None, None)), Some sil_len_expr) in let array_type, array_len = List.fold_right ~f:get_array_type_len sil_len_exprs ~init:(content_type, None) in let array_size = Exp.Sizeof {typ=array_type; nbytes=None; diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 984c4aa17..025fffde3 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -69,7 +69,7 @@ let rec get_named_type vt : Typ.t = match ot with | JBasics.TArray vt -> let content_type = get_named_type vt in - Typ.mk (Tptr (Typ.mk (Tarray (content_type, None)), Typ.Pk_pointer)) + Typ.mk (Tptr (Typ.mk (Tarray (content_type, None, None)), Typ.Pk_pointer)) | JBasics.TClass cn -> Typ.mk (Tptr (Typ.mk (Tstruct (typename_of_classname cn)), Typ.Pk_pointer)) end @@ -84,7 +84,7 @@ let extract_cn_type_np typ = let rec create_array_type typ dim = if dim > 0 then let content_typ = create_array_type typ (dim - 1) in - Typ.mk (Tptr(Typ.mk (Tarray (content_typ, None)), Typ.Pk_pointer)) + Typ.mk (Tptr(Typ.mk (Tarray (content_typ, None, None)), Typ.Pk_pointer)) else typ let extract_cn_no_obj typ = @@ -364,7 +364,7 @@ let rec object_type program tenv ot = match ot with | JBasics.TClass cn -> get_class_type program tenv cn | JBasics.TArray at -> - Typ.mk (Tptr (Typ.mk (Tarray (value_type program tenv at, None)), Typ.Pk_pointer)) + Typ.mk (Tptr (Typ.mk (Tarray (value_type program tenv at, None, None)), Typ.Pk_pointer)) (** translate a value type *) and value_type program tenv vt = @@ -410,7 +410,7 @@ let get_var_type context var = let extract_array_type typ = match typ.Typ.desc with - | Typ.Tptr({desc=Tarray (vtyp, _)}, Typ.Pk_pointer) -> vtyp + | Typ.Tptr({desc=Tarray (vtyp, _, _)}, Typ.Pk_pointer) -> vtyp | _ -> typ diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index 181a12a69..b5eab55fa 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -22,7 +22,7 @@ let tests = let yF = make_access_path "y" ["f"] in let xArr = let dummy_typ = Typ.mk Tvoid in - let dummy_arr_typ = Typ.mk (Tarray (dummy_typ, None)) in + let dummy_arr_typ = Typ.mk (Tarray (dummy_typ, None, None)) in let base = make_base "x" ~typ:dummy_arr_typ in base, [make_array_access dummy_typ] in diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index b10ae7171..775a818cf 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -8,6 +8,6 @@ codetoanalyze/c/bufferoverrun/goto_loop.c, goto_loop, 11, BUFFER_OVERRUN, [Offse codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN, [Offset: [0, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop.c:20:7] codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/nested_loop_with_label.c:19:5] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [1, 1] @ codetoanalyze/c/bufferoverrun/prune_alias.c:107:5] -codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:13:5] +codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 4, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, 0] @ codetoanalyze/c/bufferoverrun/sizeof.c:16:5] codetoanalyze/c/bufferoverrun/trivial.c, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/trivial.c:15:3] codetoanalyze/c/bufferoverrun/while_loop.c, while_loop, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [10, 10] @ codetoanalyze/c/bufferoverrun/while_loop.c:16:10] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c index ec882a3d2..c7dc892f5 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c @@ -6,6 +6,9 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ + +#include + void eval_sizeof_bad() { if (sizeof(long long) < 10000) { // always true @@ -13,3 +16,20 @@ void eval_sizeof_bad() { a[1]; // report } } + +struct some_struct { + int x0; + int x1; +}; + +void FN_static_stride_bad() { + struct some_struct a[10]; + struct some_struct *x, *y; + x = &(a[5]); + y = &(a[4]); + if (sizeof(struct some_struct) == x - y) { + // always true, but inferbo sends all pointer arithmetic to _|_ (t18130404) + int a[0]; + a[1]; // report + } +} diff --git a/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot b/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot index 50839a4d4..e08bb8228 100644 --- a/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot +++ b/infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot @@ -1,6 +1,6 @@ /* @generated */ digraph iCFG { -"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: a:int[3][2] z:int \n DECLARE_LOCALS(&return,&a,&z); [line 10]\n " color=yellow style=filled] +"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: a:int[3*32][2*96] z:int \n DECLARE_LOCALS(&return,&a,&z); [line 10]\n " color=yellow style=filled] "main.fad58de7366495db4650cfefac2fcd61_1" -> "main.fad58de7366495db4650cfefac2fcd61_3" ; diff --git a/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot b/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot index e5b14625a..79aca8939 100644 --- a/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot +++ b/infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot @@ -1,6 +1,6 @@ /* @generated */ digraph iCFG { -"vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_1" [label="1: Start vaarg_foo\nFormals: x:int\nLocals: val:int i:int valist:void[1] \n DECLARE_LOCALS(&return,&val,&i,&valist); [line 12]\n " color=yellow style=filled] +"vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_1" [label="1: Start vaarg_foo\nFormals: x:int\nLocals: val:int i:int valist:void[1*192] \n DECLARE_LOCALS(&return,&val,&i,&valist); [line 12]\n " color=yellow style=filled] "vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_1" -> "vaarg_foo.73af1e8d32c2d09f7488c5fea173b853_12" ; diff --git a/infer/tests/codetoanalyze/cpp/shared/constructors/constructor_array.cpp.dot b/infer/tests/codetoanalyze/cpp/shared/constructors/constructor_array.cpp.dot index 457b139e5..48e16a2bd 100644 --- a/infer/tests/codetoanalyze/cpp/shared/constructors/constructor_array.cpp.dot +++ b/infer/tests/codetoanalyze/cpp/shared/constructors/constructor_array.cpp.dot @@ -1,6 +1,6 @@ /* @generated */ digraph iCFG { -"array_of_person#_Z15array_of_personv.7c553fa3272204bd300dabdf4e138df7_1" [label="1: Start array_of_person\nFormals: \nLocals: arr:Person[10] 0$?%__sil_tmpSIL_materialize_temp__n$1:Person 0$?%__sil_tmpSIL_materialize_temp__n$2:Person 0$?%__sil_tmpSIL_materialize_temp__n$3:Person \n DECLARE_LOCALS(&return,&arr,&0$?%__sil_tmpSIL_materialize_temp__n$1,&0$?%__sil_tmpSIL_materialize_temp__n$2,&0$?%__sil_tmpSIL_materialize_temp__n$3); [line 17]\n " color=yellow style=filled] +"array_of_person#_Z15array_of_personv.7c553fa3272204bd300dabdf4e138df7_1" [label="1: Start array_of_person\nFormals: \nLocals: arr:Person[10*32] 0$?%__sil_tmpSIL_materialize_temp__n$1:Person 0$?%__sil_tmpSIL_materialize_temp__n$2:Person 0$?%__sil_tmpSIL_materialize_temp__n$3:Person \n DECLARE_LOCALS(&return,&arr,&0$?%__sil_tmpSIL_materialize_temp__n$1,&0$?%__sil_tmpSIL_materialize_temp__n$2,&0$?%__sil_tmpSIL_materialize_temp__n$3); [line 17]\n " color=yellow style=filled] "array_of_person#_Z15array_of_personv.7c553fa3272204bd300dabdf4e138df7_1" -> "array_of_person#_Z15array_of_personv.7c553fa3272204bd300dabdf4e138df7_4" ; @@ -15,7 +15,7 @@ digraph iCFG { "array_of_person#_Z15array_of_personv.7c553fa3272204bd300dabdf4e138df7_4" -> "array_of_person#_Z15array_of_personv.7c553fa3272204bd300dabdf4e138df7_3" ; -"matrix_of_person#_Z16matrix_of_personv.39f4dcf0df55c7259a99fabe8ccde35d_1" [label="1: Start matrix_of_person\nFormals: \nLocals: arr:Person[2][2] 0$?%__sil_tmpSIL_materialize_temp__n$1:Person 0$?%__sil_tmpSIL_materialize_temp__n$2:Person 0$?%__sil_tmpSIL_materialize_temp__n$3:Person 0$?%__sil_tmpSIL_materialize_temp__n$4:Person \n DECLARE_LOCALS(&return,&arr,&0$?%__sil_tmpSIL_materialize_temp__n$1,&0$?%__sil_tmpSIL_materialize_temp__n$2,&0$?%__sil_tmpSIL_materialize_temp__n$3,&0$?%__sil_tmpSIL_materialize_temp__n$4); [line 22]\n " color=yellow style=filled] +"matrix_of_person#_Z16matrix_of_personv.39f4dcf0df55c7259a99fabe8ccde35d_1" [label="1: Start matrix_of_person\nFormals: \nLocals: arr:Person[2*32][2*64] 0$?%__sil_tmpSIL_materialize_temp__n$1:Person 0$?%__sil_tmpSIL_materialize_temp__n$2:Person 0$?%__sil_tmpSIL_materialize_temp__n$3:Person 0$?%__sil_tmpSIL_materialize_temp__n$4:Person \n DECLARE_LOCALS(&return,&arr,&0$?%__sil_tmpSIL_materialize_temp__n$1,&0$?%__sil_tmpSIL_materialize_temp__n$2,&0$?%__sil_tmpSIL_materialize_temp__n$3,&0$?%__sil_tmpSIL_materialize_temp__n$4); [line 22]\n " color=yellow style=filled] "matrix_of_person#_Z16matrix_of_personv.39f4dcf0df55c7259a99fabe8ccde35d_1" -> "matrix_of_person#_Z16matrix_of_personv.39f4dcf0df55c7259a99fabe8ccde35d_4" ; @@ -30,7 +30,7 @@ digraph iCFG { "matrix_of_person#_Z16matrix_of_personv.39f4dcf0df55c7259a99fabe8ccde35d_4" -> "matrix_of_person#_Z16matrix_of_personv.39f4dcf0df55c7259a99fabe8ccde35d_3" ; -"initialization_c_style#_Z22initialization_c_stylev.6b9bfbb6779ee90799bffc017bfd501e_1" [label="1: Start initialization_c_style\nFormals: \nLocals: z2:Z z:Z[2] \n DECLARE_LOCALS(&return,&z2,&z); [line 32]\n " color=yellow style=filled] +"initialization_c_style#_Z22initialization_c_stylev.6b9bfbb6779ee90799bffc017bfd501e_1" [label="1: Start initialization_c_style\nFormals: \nLocals: z2:Z z:Z[2*64] \n DECLARE_LOCALS(&return,&z2,&z); [line 32]\n " color=yellow style=filled] "initialization_c_style#_Z22initialization_c_stylev.6b9bfbb6779ee90799bffc017bfd501e_1" -> "initialization_c_style#_Z22initialization_c_stylev.6b9bfbb6779ee90799bffc017bfd501e_4" ; @@ -45,7 +45,7 @@ digraph iCFG { "initialization_c_style#_Z22initialization_c_stylev.6b9bfbb6779ee90799bffc017bfd501e_4" -> "initialization_c_style#_Z22initialization_c_stylev.6b9bfbb6779ee90799bffc017bfd501e_3" ; -"initialization_mixed_styles_not_handled_correctly#_Z49initialization_mixed_styles_not_handled_correc.e1de50291cecd2ac4e0ba29b88e060a6_1" [label="1: Start initialization_mixed_styles_not_handled_correctly\nFormals: \nLocals: z2:Z z:Z[2] old:Z \n DECLARE_LOCALS(&return,&z2,&z,&old); [line 39]\n " color=yellow style=filled] +"initialization_mixed_styles_not_handled_correctly#_Z49initialization_mixed_styles_not_handled_correc.e1de50291cecd2ac4e0ba29b88e060a6_1" [label="1: Start initialization_mixed_styles_not_handled_correctly\nFormals: \nLocals: z2:Z z:Z[2*64] old:Z \n DECLARE_LOCALS(&return,&z2,&z,&old); [line 39]\n " color=yellow style=filled] "initialization_mixed_styles_not_handled_correctly#_Z49initialization_mixed_styles_not_handled_correc.e1de50291cecd2ac4e0ba29b88e060a6_1" -> "initialization_mixed_styles_not_handled_correctly#_Z49initialization_mixed_styles_not_handled_correc.e1de50291cecd2ac4e0ba29b88e060a6_5" ; diff --git a/infer/tests/codetoanalyze/cpp/shared/constructors/std_init_list.cpp.dot b/infer/tests/codetoanalyze/cpp/shared/constructors/std_init_list.cpp.dot index d0242023b..f16ae027f 100644 --- a/infer/tests/codetoanalyze/cpp/shared/constructors/std_init_list.cpp.dot +++ b/infer/tests/codetoanalyze/cpp/shared/constructors/std_init_list.cpp.dot @@ -1,13 +1,13 @@ /* @generated */ digraph iCFG { -"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: x:X 0$?%__sil_tmpSIL_materialize_temp__n$0:int const [5] const \n DECLARE_LOCALS(&return,&x,&0$?%__sil_tmpSIL_materialize_temp__n$0); [line 24]\n " color=yellow style=filled] +"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: x:X 0$?%__sil_tmpSIL_materialize_temp__n$0:int const [5*32] const \n DECLARE_LOCALS(&return,&x,&0$?%__sil_tmpSIL_materialize_temp__n$0); [line 24]\n " color=yellow style=filled] "main.fad58de7366495db4650cfefac2fcd61_1" -> "main.fad58de7366495db4650cfefac2fcd61_3" ; "main.fad58de7366495db4650cfefac2fcd61_2" [label="2: Exit main \n " color=yellow style=filled] -"main.fad58de7366495db4650cfefac2fcd61_3" [label="3: DeclStmt \n *&0$?%__sil_tmpSIL_materialize_temp__n$0[0]:int const =1 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[1]:int const =2 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[2]:int const =3 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[3]:int const =4 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[4]:int const =5 [line 24]\n n$1=_fun___infer_skip_function(&0$?%__sil_tmpSIL_materialize_temp__n$0:int const [5] const ) [line 24]\n _fun_X_X(&x:X*,n$1:std::initializer_list) [line 24]\n " shape="box"] +"main.fad58de7366495db4650cfefac2fcd61_3" [label="3: DeclStmt \n *&0$?%__sil_tmpSIL_materialize_temp__n$0[0]:int const =1 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[1]:int const =2 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[2]:int const =3 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[3]:int const =4 [line 24]\n *&0$?%__sil_tmpSIL_materialize_temp__n$0[4]:int const =5 [line 24]\n n$1=_fun___infer_skip_function(&0$?%__sil_tmpSIL_materialize_temp__n$0:int const [5*32] const ) [line 24]\n _fun_X_X(&x:X*,n$1:std::initializer_list) [line 24]\n " shape="box"] "main.fad58de7366495db4650cfefac2fcd61_3" -> "main.fad58de7366495db4650cfefac2fcd61_2" ; diff --git a/infer/tests/codetoanalyze/objc/frontend/vardecl/initlist.m.dot b/infer/tests/codetoanalyze/objc/frontend/vardecl/initlist.m.dot index 869b6afd3..40eacf705 100644 --- a/infer/tests/codetoanalyze/objc/frontend/vardecl/initlist.m.dot +++ b/infer/tests/codetoanalyze/objc/frontend/vardecl/initlist.m.dot @@ -1,6 +1,6 @@ /* @generated */ digraph iCFG { -"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: a:int[3][2] z:int \n DECLARE_LOCALS(&return,&a,&z); [line 12]\n " color=yellow style=filled] +"main.fad58de7366495db4650cfefac2fcd61_1" [label="1: Start main\nFormals: \nLocals: a:int[3*32][2*96] z:int \n DECLARE_LOCALS(&return,&a,&z); [line 12]\n " color=yellow style=filled] "main.fad58de7366495db4650cfefac2fcd61_1" -> "main.fad58de7366495db4650cfefac2fcd61_3" ; @@ -11,7 +11,7 @@ digraph iCFG { "main.fad58de7366495db4650cfefac2fcd61_3" -> "main.fad58de7366495db4650cfefac2fcd61_2" ; -"test.098f6bcd4621d373cade4e832627b4f6_1" [label="1: Start test\nFormals: \nLocals: a:C*[3] c2:C* c1:C* \n DECLARE_LOCALS(&return,&a,&c2,&c1); [line 21]\n " color=yellow style=filled] +"test.098f6bcd4621d373cade4e832627b4f6_1" [label="1: Start test\nFormals: \nLocals: a:C*[3*64] c2:C* c1:C* \n DECLARE_LOCALS(&return,&a,&c2,&c1); [line 21]\n " color=yellow style=filled] "test.098f6bcd4621d373cade4e832627b4f6_1" -> "test.098f6bcd4621d373cade4e832627b4f6_5" ;