Commit 31942261 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Stylistic fixes in misc.ml and located in ptr_index

parent 7e8028ae
......@@ -269,27 +269,22 @@ let arith_op = function
| IndexPI -> PlusA
| _ -> assert false
let rec ptr_index ?(index=(Cil.zero Location.unknown)) exp =
(* ****************************************************************** *)
let rec ptr_index ?(loc=Location.unknown) ?(index=(Cil.zero loc)) exp =
match exp.enode with
| BinOp(op, lhs, rhs, _) ->
(match op with
(* Pointer arithmetic: split pointer and integer parts *)
| MinusPI | PlusPI | IndexPI ->
let index = Cil.mkBinOp Location.unknown (arith_op op) index rhs
in ptr_index ~index lhs
let index = Cil.mkBinOp loc (arith_op op) index rhs in
ptr_index ~index lhs
(* Other arithmetic: treat the whole expression as pointer address *)
| MinusPP | PlusA | MinusA | Mult | Div | Mod ->
(exp, index)
| _ -> assert false)
(* ****************************************************************** *)
| CastE(_) -> ptr_index ~index (Cil.stripCasts exp)
(* ****************************************************************** *)
| Const(_)
| StartOf(_)
| AddrOf(_)
| Lval(_) -> (exp, index)
| _ -> assert false
| CastE _ -> ptr_index ~index (Cil.stripCasts exp)
| Const _ | StartOf _ | AddrOf _ | Lval _ -> (exp, index)
| SizeOf _| SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ | UnOp _
| Info _ -> assert false
(*
Local Variables:
......
......@@ -89,7 +89,7 @@ val reorder_ast: unit -> unit
val cty: logic_type -> typ
(* Assume that the logic type is indeed a C type. Just return it. *)
val ptr_index: ?index:Cil_types.exp -> Cil_types.exp
val ptr_index: ?loc:location -> ?index:exp -> exp
-> Cil_types.exp * Cil_types.exp
(** Split pointer-arithmetic expression of the type `p + i` into its
pointer and integer parts. *)
......
......@@ -584,14 +584,14 @@ and mmodel_call_with_size ~loc kf name ctx env t =
(fun v _ ->
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = (Misc.mk_api_name name) in
let fname = Misc.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
in
res, env
and mmodel_call_valid ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index e in
let base, _ = Misc.ptr_index ~loc e in
let _, res, env =
Env.new_var
~loc
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment