Skip to content
Open
Show file tree
Hide file tree
Changes from 5 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
3 changes: 1 addition & 2 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
Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bot_value was an odd one out that had this unrollType for the TNamed case, others didn't so I removed it from here as well.
Technically, unrollType does propagate the attributes but these functions haven't done that before so I'm not sure if it's actually needed for anything. I left TODOs about this just in case.

| _ -> Bot

let is_bot_value x =
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