File tree Expand file tree Collapse file tree 1 file changed +6
-9
lines changed
Expand file tree Collapse file tree 1 file changed +6
-9
lines changed Original file line number Diff line number Diff line change @@ -2188,15 +2188,12 @@ struct
21882188 (* | _ -> ignore @@ Pretty.printf "strcpy: dst %a may point to anything!\n" d_exp dst; *)
21892189 (* ctx.local *)
21902190 (* end *)
2191- let rec get_lval exp = match stripCasts exp with
2192- | Lval x | AddrOf x | StartOf x -> x
2193- | BinOp (PlusPI , e, i, _)
2194- | BinOp (MinusPI, e , i , _ ) -> get_lval e
2195- | x ->
2196- ignore @@ Pretty. printf " strcpy: dst is %a!\n " d_plainexp dst;
2197- failwith " strcpy: expecting first argument to be a pointer!"
2198- in
2199- assign ctx (get_lval dst) src
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
2195+ let value = VD. top_value dest_typ in
2196+ set ~ctx: (Some ctx) (Analyses. ask_of_ctx ctx) gs st dest_a dest_typ value
22002197 | _ -> failwith " strcpy arguments are strange/complicated."
22012198 end
22022199 | `Unknown "F1" ->
You can’t perform that action at this time.
0 commit comments