Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Comment thread
sim642 marked this conversation as resolved.
in
set ~man st dest_a dest_typ value in
(* for string functions *)
Expand Down Expand Up @@ -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)
Comment thread
sim642 marked this conversation as resolved.
end
(* else compute value in array domain *)
else
Expand Down Expand Up @@ -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)
Comment thread
sim642 marked this conversation as resolved.
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)
Comment thread
sim642 marked this conversation as resolved.
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 =
Expand Down Expand Up @@ -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
Comment thread
sim642 marked this conversation as resolved.
in
set ~man st dest_a dest_typ value
) st lv
Expand Down
11 changes: 3 additions & 8 deletions src/analyses/memLeak.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
9 changes: 4 additions & 5 deletions src/cdomain/value/cdomains/valueDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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 =
Expand All @@ -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) =
Expand Down Expand Up @@ -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
Expand Down
8 changes: 2 additions & 6 deletions src/cdomains/unionFind.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 5 additions & 0 deletions src/common/util/cilfacade.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading