@@ -2134,6 +2134,11 @@ struct
21342134 invalidate ~ctx (Analyses. ask_of_ctx ctx) ctx.global st [Cil. mkAddrOrStartOf lv]
21352135 | None -> st
21362136 in
2137+ let addr_type_of_exp exp =
2138+ let lval = mkMem ~addr: (Cil. stripCasts exp) ~off: NoOffset in
2139+ let addr = eval_lv (Analyses. ask_of_ctx ctx) ctx.global ctx.local lval in
2140+ (addr, AD. get_type addr)
2141+ in
21372142 let forks = forkfun ctx lv f args in
21382143 if M. tracing then if not (List. is_empty forks) then M. tracel " spawn" " Base.special %s: spawning functions %a\n " f.vname (d_list " ," d_varinfo) (List. map BatTuple.Tuple3. second forks);
21392144 List. iter (BatTuple.Tuple3. uncurry ctx.spawn) forks;
@@ -2146,10 +2151,7 @@ struct
21462151 | ("memset" | "__builtin_memset" ), [dest; ch; count] ->
21472152 (* TODO: check count *)
21482153 let eval_ch = eval_rv (Analyses. ask_of_ctx ctx) gs st ch in
2149- let dest_lval = mkMem ~addr: (Cil. stripCasts dest) ~off: NoOffset in
2150- let dest_a = eval_lv (Analyses. ask_of_ctx ctx) gs st dest_lval in
2151- (* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
2152- let dest_typ = AD. get_type dest_a in (* TODO: what is the right way? *)
2154+ let dest_a, dest_typ = addr_type_of_exp dest in
21532155 let value =
21542156 match eval_ch with
21552157 | `Int i when ID. to_int i = Some Z. zero ->
@@ -2166,10 +2168,7 @@ struct
21662168 | " __explicit_bzero_chk" , [dest; count; _ (* dest_size *) ]
21672169 | ("bzero" | "__builtin_bzero" | "explicit_bzero" ), [dest; count] ->
21682170 (* TODO: check count *)
2169- let dest_lval = mkMem ~addr: (Cil. stripCasts dest) ~off: NoOffset in
2170- let dest_a = eval_lv (Analyses. ask_of_ctx ctx) gs st dest_lval in
2171- (* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
2172- let dest_typ = AD. get_type dest_a in (* TODO: what is the right way? *)
2171+ let dest_a, dest_typ = addr_type_of_exp dest in
21732172 let value = VD. zero_init_value dest_typ in
21742173 set ~ctx: (Some ctx) (Analyses. ask_of_ctx ctx) gs st dest_a dest_typ value
21752174 | _ , _ -> failwith " strange bzero arguments"
@@ -2188,10 +2187,7 @@ struct
21882187 (* | _ -> ignore @@ Pretty.printf "strcpy: dst %a may point to anything!\n" d_exp dst; *)
21892188 (* ctx.local *)
21902189 (* end *)
2191- let dest_lval = mkMem ~addr: (Cil. stripCasts dst) ~off: NoOffset in
2192- let dest_a = eval_lv (Analyses. ask_of_ctx ctx) gs st dest_lval in
2193- (* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
2194- let dest_typ = AD. get_type dest_a in
2190+ let dest_a, dest_typ = addr_type_of_exp dst in
21952191 let value = VD. top_value dest_typ in
21962192 set ~ctx: (Some ctx) (Analyses. ask_of_ctx ctx) gs st dest_a dest_typ value
21972193 | _ -> failwith " strcpy arguments are strange/complicated."
0 commit comments