File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -2413,9 +2413,7 @@ struct
24132413 | _ -> false
24142414 in
24152415 let dest_a, dest_typ = addr_type_of_exp dst in
2416- let src_lval = mkMem ~addr: (Cil. stripCasts src) ~off: NoOffset in
2417- let src_typ = eval_lv ~man man.local src_lval
2418- |> AD. type_of in
2416+ let _, src_typ = addr_type_of_exp src in
24192417 (* when src and destination type coincide, take value from the source, otherwise use top *)
24202418 let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then
24212419 (* TODO: why cast if types coincide? *)
@@ -2627,13 +2625,7 @@ struct
26272625 raise Deadcode
26282626 | MutexAttrSetType {attr = attr ; typ = mtyp } , _ ->
26292627 begin
2630- let get_type lval =
2631- let address = eval_lv ~man st lval in
2632- AD. type_of address
2633- in
2634- let dst_lval = mkMem ~addr: (Cil. stripCasts attr) ~off: NoOffset in
2635- let dest_typ = get_type dst_lval in
2636- let dest_a = eval_lv ~man st dst_lval in
2628+ let dest_a, dest_typ = addr_type_of_exp attr in
26372629 let fallback () = set ~man st dest_a ~lval_type: dest_typ (MutexAttr (ValueDomain.MutexAttr. top () )) in
26382630 match eval_rv ~man st mtyp with
26392631 | Int x ->
You can’t perform that action at this time.
0 commit comments