Skip to content
Snippets Groups Projects
Commit 46b1abf5 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Update `Misc.base_ptr` call sites

parent 193a87cd
No related branches found
No related tags found
No related merge requests found
...@@ -507,12 +507,12 @@ let call_valid ~loc kf name ctx env t p = ...@@ -507,12 +507,12 @@ let call_valid ~loc kf name ctx env t p =
assert (name = "valid" || name = "valid_read"); assert (name = "valid" || name = "valid_read");
let arg_from_term ~loc kf env rev_args t _p = let arg_from_term ~loc kf env rev_args t _p =
let ptr, size, env = term_to_ptr_and_size ~loc kf env t in let ptr, size, env = term_to_ptr_and_size ~loc kf env t in
let base, base_addr = Misc.ptr_base ~loc ptr in let base, base_addr = Misc.ptr_base_and_base_addr ~loc ptr in
base_addr :: base :: size :: ptr :: rev_args, env base_addr :: base :: size :: ptr :: rev_args, env
in in
let arg_from_range ~loc kf env rev_args ptr r p = let arg_from_range ~loc kf env rev_args ptr r p =
let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in let ptr, size, env = range_to_ptr_and_size ~loc kf env ptr r p in
let base, base_addr = Misc.ptr_base ~loc ptr in let base, base_addr = Misc.ptr_base_and_base_addr ~loc ptr in
base_addr :: base :: size :: ptr :: rev_args, env base_addr :: base :: size :: ptr :: rev_args, env
in in
let prepend_n_args = false in let prepend_n_args = false in
......
...@@ -146,9 +146,9 @@ let assign ?(ltype) lhs rhs loc = ...@@ -146,9 +146,9 @@ let assign ?(ltype) lhs rhs loc =
in in
match Cil.unrollType ltype with match Cil.unrollType ltype with
| TPtr _ -> | TPtr _ ->
let base, _ = Misc.ptr_index rhs in let base = Misc.ptr_base ~loc:rhs.eloc rhs in
let rhs, flow = let rhs, flow =
(match base.enode with (match (Cil.stripCasts base).enode with
| AddrOf _ | AddrOf _
| StartOf _ -> rhs, Direct | StartOf _ -> rhs, Direct
(* Unary operator describes !, ~ or -: treat it same as Const since (* Unary operator describes !, ~ or -: treat it same as Const since
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment