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

[IR] add stride to array type

Browse Source 
Summary:
An array has a static or dynamic length (number of elements), but it also has a
stride, determined by the type of the element: `sizeof(element_type)`. We don't
have a good `sizeof()` function available on SIL types, so record that stride
in the array type.

update-submodule: facebook-clang-plugins

Reviewed By: mbouaziz

Differential Revision: D4969697

fbshipit-source-id: 98e0670
master
Jules Villard 8 years ago committed by Facebook Github Bot
parent 9910391144
commit 93ec47a5f4
30 changed files with 138 additions and 116 deletions
Show Stats Download Patch File Download Diff File

2
facebook-clang-plugins

@ -1 +1 @@
Subproject commit c7e476c39601eaf3ccaff272006c7da799cac208
Subproject commit 84b3c58ab12fd42779ea4f8c1214432801cf4a5f

22
infer/src/IR/Typ.re
Unescape View File

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

8
infer/src/IR/Typ.rei
Unescape View File

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

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

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

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

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

6
infer/src/backend/dom.ml
Unescape View File

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

2
infer/src/backend/dotty.ml
Unescape View File

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

20
infer/src/backend/prop.ml
Unescape View File

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

15
infer/src/backend/prover.ml
Unescape View File

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

28
infer/src/backend/rearrange.ml
Unescape View File

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

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

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

2
infer/src/bufferoverrun/arrayBlk.ml
Unescape View File

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

21
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

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

3
infer/src/bufferoverrun/bufferOverrunSemantics.ml
Unescape View File

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

2
infer/src/checkers/accessPath.ml
Unescape View File

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

3
infer/src/clang/ast_expressions.ml
Unescape View File

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

13
infer/src/clang/cTrans.ml
Unescape View File

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

2
infer/src/clang/cTrans_utils.ml
Unescape View File

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

21
infer/src/clang/cType_to_sil_type.ml
Unescape View File

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

4
infer/src/harness/inhabit.ml
Unescape View File

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

4
infer/src/java/jTrans.ml
Unescape View File

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

8
infer/src/java/jTransType.ml
Unescape View File

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

2
infer/src/unit/accessPathTests.ml
Unescape View File

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

2
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

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

20
infer/tests/codetoanalyze/c/bufferoverrun/sizeof.c
Unescape View File

@ -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 <stdlib.h>
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
}
}

2
infer/tests/codetoanalyze/c/frontend/initialization/array_initlistexpr.c.dot
Unescape View File

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

2
infer/tests/codetoanalyze/c/frontend/vaarg_expr/vaarg_expr.c.dot
Unescape View File

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

8
infer/tests/codetoanalyze/cpp/shared/constructors/constructor_array.cpp.dot
Unescape View File

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

4
infer/tests/codetoanalyze/cpp/shared/constructors/std_init_list.cpp.dot
Unescape View File

@ -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<int>) [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<int>) [line 24]\n " shape="box"]
"main.fad58de7366495db4650cfefac2fcd61_3" -> "main.fad58de7366495db4650cfefac2fcd61_2" ;

4
infer/tests/codetoanalyze/objc/frontend/vardecl/initlist.m.dot
Unescape View File

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

Write Preview
Loading…
Cancel
Save