diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 80572a3b14..2b281eff69 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2419,7 +2419,7 @@ struct let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~kind:Internal ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in eval_rv ~man st (Lval src_cast_lval) else - VD.top_value (unrollType dest_typ) + VD.top_value dest_typ in set ~man st dest_a dest_typ value in (* for string functions *) @@ -2471,11 +2471,11 @@ struct else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *) set ~man st lv_a lv_typ (f s1_a s2_a) else - set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + set ~man st lv_a lv_typ (VD.top_value lv_typ) | _ -> (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *) let _ = AD.string_writing_defined s1_a in - set ~man st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + set ~man st s1_a s1_typ (VD.top_value s1_typ) end (* else compute value in array domain *) else @@ -2513,13 +2513,13 @@ struct if op_addr = None then (* triggers warning, function only evaluated for side-effects *) let _ = AD.string_writing_defined s1_a in - set ~man st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + set ~man st s1_a s1_typ (VD.top_value s1_typ) else let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in set ~man st lv_a lv_typ (op_array array_s1 array_s2) | _ -> - set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + set ~man st lv_a lv_typ (VD.top_value lv_typ) in (* Returns a tuple, the first is the address of the blob if one was allocated, the second is the returned address (may contain null pointer or be only null-pointer) *) let alloc loc size = @@ -2583,7 +2583,7 @@ struct else match get ~man st a None with | Array array_s -> Int (CArrays.to_string_length array_s) - | _ -> VD.top_value (unrollType dest_typ) + | _ -> VD.top_value dest_typ in set ~man st dest_a dest_typ value ) st lv diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index c86f3c4ff6..ffce06d3e9 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -34,18 +34,13 @@ struct |> List.filter (fun v -> match unrollType v.vtype with | TPtr (TComp (ci,_), _) - | TPtr ((TNamed ({ttype = TComp (ci, _); _}, _)), _) -> ci.cstruct - | TComp (_, _) - | (TNamed ({ttype = TComp _; _}, _)) -> false + | TPtr ((TNamed ({ttype = TComp (ci, _); _}, _)), _) -> ci.cstruct (* TODO: unrollTypeDeep? *) + | TComp (_, _) -> false | _ -> false) let get_global_struct_non_ptr_vars () = get_global_vars () - |> List.filter (fun v -> - match unrollType v.vtype with - | TComp (ci, _) - | (TNamed ({ttype = TComp (ci,_); _}, _)) -> ci.cstruct - | _ -> false) + |> List.filter (fun v -> Cilfacade.isStructType v.vtype) let get_reachable_mem_from_globals (global_vars:varinfo list) man = global_vars diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 761476fef0..1b998496be 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -167,8 +167,7 @@ struct Array (CArrays.make ~varAttr ~typAttr len (bot_value ai)) | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ()) | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.bot ()) - | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false) - | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t) + | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr t (* TODO: Should this add attributes from TNamed to t like unrollType? *) | _ -> Bot let is_bot_value x = @@ -204,7 +203,7 @@ struct let len = array_length_idx (IndexDomain.bot ()) length in Array (CArrays.make ~varAttr ~typAttr len (if can_recover_from_top then (init_value ai) else (bot_value ai))) (* | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ()) *) - | TNamed ({ttype=t; _}, _) -> init_value ~varAttr t + | TNamed ({ttype=t; _}, _) -> init_value ~varAttr t (* TODO: Should this add attributes from TNamed to t like unrollType? *) | _ -> Top let rec top_value ?(varAttr=[]) (t: typ): t = @@ -222,7 +221,7 @@ struct let typAttr = typeAttrs ai in let len = array_length_idx (IndexDomain.top ()) length in Array (CArrays.make ~varAttr ~typAttr len (top_value ai)) - | TNamed ({ttype=t; _}, _) -> top_value ~varAttr t + | TNamed ({ttype=t; _}, _) -> top_value ~varAttr t (* TODO: Should this add attributes from TNamed to t like unrollType? *) | _ -> Top let is_top_value x (t: typ) = @@ -266,7 +265,7 @@ struct let len = array_length_idx (IndexDomain.top ()) length in Array (CArrays.make ~varAttr ~typAttr len (zero_init_value ai)) (* | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ()) *) - | TNamed ({ttype=t; _}, _) -> zero_init_value ~varAttr t + | TNamed ({ttype=t; _}, _) -> zero_init_value ~varAttr t (* TODO: Should this add attributes from TNamed to t like unrollType? *) | _ -> Top let show_tag : t -> string = function diff --git a/src/cdomains/unionFind.ml b/src/cdomains/unionFind.ml index 585ea117ca..a56795d293 100644 --- a/src/cdomains/unionFind.ml +++ b/src/cdomains/unionFind.ml @@ -193,12 +193,8 @@ module T = struct | None -> Z.one - let is_struct_type t = - match Cil.unrollType t with - | TComp _ -> - true - | _ -> - false + (* TODO: Should this actually be accounting for unions? *) + let is_struct_type = Cilfacade.isStructOrUnionType let is_struct_ptr_type t = match Cil.unrollType t with diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 7fefc3fd14..d43e77dabb 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -49,6 +49,11 @@ let isStructOrUnionType t = | TComp _ -> true | _ -> false +let isStructType t = + match Cil.unrollType t with + | TComp (ci, _) -> ci.cstruct + | _ -> false + let is_first_field x = match x.fcomp.cfields with | [] -> false | f :: _ -> CilType.Fieldinfo.equal f x