diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index cc500b933b13597f00acacc76e3aa51d0c790b0f..ccbe1f20c772b588235a497545701421effd9558 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -208,7 +208,7 @@ let rec is_dangerous_offset = function
let rec is_dangerous e = match e.enode with
| Lval lv | AddrOf lv | StartOf lv -> is_dangerous_lval lv
- | UnOp (_,e,_) | CastE(_,e) | Info(e,_) -> is_dangerous e
+ | UnOp (_,e,_) | CastE(_,e) -> is_dangerous e
| BinOp(_,e1,e2,_) -> is_dangerous e1 || is_dangerous e2
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
false
@@ -1379,12 +1379,12 @@ let rec is_boolean_result e =
| None -> false)
| CastE (_,e) -> is_boolean_result e
| BinOp((Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr),_,_,_) -> true
- | BinOp((PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP | Mult
+ | BinOp((PlusA | PlusPI | MinusA | MinusPI | MinusPP | Mult
| Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr),_,_,_) -> false
| UnOp(LNot,_,_) -> true
| UnOp ((Neg | BNot),_,_) -> false
| Lval _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _
- | AlignOfE _ | AddrOf _ | StartOf _ | Info _ -> false
+ | AlignOfE _ | AddrOf _ | StartOf _ -> false
(* Like Cil.mkCastT, but it calls typeForInsertedCast *)
let makeCastT ~(e: exp) ~(oldt: typ) ~(newt: typ) =
@@ -5920,7 +5920,7 @@ and doExp local_env
addOffsetLval (Index(e2'', NoOffset)) array
| _ -> (* Turn into *(e1 + e2) *)
mkMem
- (new_exp ~loc:e1''.eloc (BinOp(IndexPI, e1'', e2'', t1)))
+ (new_exp ~loc:e1''.eloc (BinOp(PlusPI, e1'', e2'', t1)))
NoOffset
in
(* Do some optimization of StartOf *)
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 1f798027f2b6803d8a9987ee8394323a902c3d14..8f13b954a39d7337a3a5e7eca15af4964316c234 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -698,15 +698,6 @@ and exp_node =
[TPtr(T)]. In C this operation is implicit, the [StartOf] operator is not
printed. We have it in CIL because it makes the typing rules simpler. *)
- | Info of exp * exp_info
- (** Additional information on the underlying expression *)
-
-(** Additional information on an expression *)
-and exp_info = {
- exp_type : logic_type; (** when used as placeholder for a term *)
- exp_name: string list;
-}
-
(* ************************************************************************* *)
(** {2 Constants} *)
(* ************************************************************************* *)
@@ -759,12 +750,6 @@ and unop =
and binop =
PlusA (** arithmetic + *)
| PlusPI (** pointer + integer *)
- | IndexPI (** pointer + integer but only when it arises from an expression
- [e\[i\]] when [e] is a pointer and
- not an array. This is semantically
- the same as PlusPI but CCured uses
- this as a hint that the integer is
- probably positive. *)
| MinusA (** arithmetic - *)
| MinusPI (** pointer - integer *)
| MinusPP (** pointer - pointer *)
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index 041ad81546544c1a946bc4dae5fba040bdd471fd..4e2ba27dad635815b318f79d27b95b4b0b26f6d0 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -314,8 +314,7 @@ module Precedence = struct
(assoc_connector_level thisLevel && thisLevel == contextprec
&& not state.print_cil_as_is))
- let getParenthLevel e = match (Cil.stripInfo e).enode with
- | Info _ -> assert false
+ let getParenthLevel e = match e.enode with
| BinOp(LAnd, _,_,_) -> and_level
| BinOp(LOr, _,_,_) -> or_level
(* Bit operations. *)
@@ -325,7 +324,7 @@ module Precedence = struct
(* Additive. Shifts can have higher level than + or - but I want parentheses
around them *)
| BinOp((MinusA|MinusPP|MinusPI|PlusA|
- PlusPI|IndexPI|Shiftlt|Shiftrt),_,_,_) -> additiveLevel
+ PlusPI|Shiftlt|Shiftrt),_,_,_) -> additiveLevel
(* Multiplicative *)
| BinOp((Div|Mod|Mult),_,_,_) -> multiplicativeLevel
(* Unary *)
@@ -354,7 +353,7 @@ module Precedence = struct
(* Additive. Shifts can have higher level than + or - but I want parentheses
around them *)
| TBinOp((MinusA|MinusPP|MinusPI|PlusA|
- PlusPI|IndexPI|Shiftlt|Shiftrt),_,_) -> additiveLevel
+ PlusPI|Shiftlt|Shiftrt),_,_) -> additiveLevel
(* Multiplicative *)
| TBinOp((Div|Mod|Mult),_,_) -> multiplicativeLevel
| Tapp({ l_var_info },[],[_;_])
@@ -797,8 +796,7 @@ class cil_printer () = object (self)
parent_non_decay <- false;
let level = Precedence.getParenthLevel e in
(* fprintf fmt "/* eid:%d */" e.eid; *)
- match (Cil.stripInfo e).enode with
- | Info _ -> assert false
+ match e.enode with
| Const(c) -> self#constant fmt c
| Lval(l) -> self#lval fmt l
@@ -854,7 +852,7 @@ class cil_printer () = object (self)
method binop fmt b =
fprintf fmt "%s"
(match b with
- | PlusA | PlusPI | IndexPI -> "+"
+ | PlusA | PlusPI -> "+"
| MinusA | MinusPP | MinusPI -> "-"
| Mult -> "*"
| Div -> "/"
@@ -1001,7 +999,7 @@ class cil_printer () = object (self)
| Set(lv,e,_) -> begin
(* Be nice to some special cases *)
match e.enode with
- BinOp((PlusA|PlusPI|IndexPI),
+ BinOp((PlusA|PlusPI),
{enode = Lval(lv')},
{enode=Const(CInt64(one,_,_))},_)
when LvalStructEq.equal lv lv' && Integer.equal one Integer.one
@@ -1018,7 +1016,7 @@ class cil_printer () = object (self)
(self#lval_prec Precedence.indexLevel) lv
instr_terminator
- | BinOp((PlusA|PlusPI|IndexPI),
+ | BinOp((PlusA|PlusPI),
{enode = Lval(lv')},
{enode = Const(CInt64(mone,_,_))},_)
when LvalStructEq.equal lv lv' && Integer.equal mone Integer.minus_one
@@ -1027,7 +1025,7 @@ class cil_printer () = object (self)
(self#lval_prec Precedence.indexLevel) lv
instr_terminator
- | BinOp((PlusA|PlusPI|IndexPI|MinusA|MinusPP|MinusPI|BAnd|BOr|BXor|
+ | BinOp((PlusA|PlusPI|MinusA|MinusPP|MinusPI|BAnd|BOr|BXor|
Mult|Div|Mod|Shiftlt|Shiftrt) as bop,
{enode = Lval(lv')},e,_) when LvalStructEq.equal lv lv' ->
fprintf fmt "%a %a= %a%s"
@@ -2419,7 +2417,7 @@ class cil_printer () = object (self)
method term_binop fmt b =
fprintf fmt "%s"
(match b with
- | PlusA | PlusPI | IndexPI -> "+"
+ | PlusA | PlusPI -> "+"
| MinusA | MinusPP | MinusPI -> "-"
| Mult -> "*"
| Div -> "/"
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index f9c1724b21ea587c2532165f5f982ac4ec7f99a3..2ff6ad08971cd86179fd47ff9be974ea51fa852d 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -400,11 +400,6 @@ and pp_exp_node fmt = function
| CastE(typ,exp) -> Format.fprintf fmt "CastE(%a,%a)" pp_typ typ pp_exp exp
| AddrOf(lval) -> Format.fprintf fmt "AddrOf(%a)" pp_lval lval
| StartOf(lval) -> Format.fprintf fmt "StartOf(%a)" pp_lval lval
- | Info(exp,exp_info) -> Format.fprintf fmt "Info(%a,%a)" pp_exp exp pp_exp_info exp_info
-
-and pp_exp_info fmt exp_info = Format.fprintf fmt "{exp_type=%a;exp_name=%a}"
- pp_logic_type exp_info.exp_type
- (pp_list pp_string) exp_info.exp_name
and pp_constant fmt = function
| CInt64(integer,ikind,string_option) ->
@@ -424,7 +419,6 @@ and pp_unop fmt = function
and pp_binop fmt = function
| PlusA -> Format.fprintf fmt "PlusA"
| PlusPI -> Format.fprintf fmt "PlusPI"
- | IndexPI -> Format.fprintf fmt "IndexPI"
| MinusA -> Format.fprintf fmt "MinusA"
| MinusPI -> Format.fprintf fmt "MinusPI"
| MinusPP -> Format.fprintf fmt "MinusPP"
diff --git a/src/kernel_services/ast_printing/cil_types_debug.mli b/src/kernel_services/ast_printing/cil_types_debug.mli
index 1f9f96be7d91156fa8bd30165c5547cc98a4f271..a3354f6d42dfa38c5b969ac01d3662f1083a30e1 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.mli
+++ b/src/kernel_services/ast_printing/cil_types_debug.mli
@@ -86,7 +86,6 @@ val pp_varinfo : Cil_types.varinfo Pretty_utils.formatter
val pp_storage : Format.formatter -> Cil_types.storage -> unit
val pp_exp : Cil_types.exp Pretty_utils.formatter
val pp_exp_node : Format.formatter -> Cil_types.exp_node -> unit
-val pp_exp_info : Format.formatter -> Cil_types.exp_info -> unit
val pp_constant : Format.formatter -> Cil_types.constant -> unit
val pp_unop : Format.formatter -> Cil_types.unop -> unit
val pp_binop : Format.formatter -> Cil_types.binop -> unit
diff --git a/src/kernel_services/ast_queries/ast_info.ml b/src/kernel_services/ast_queries/ast_info.ml
index bb5c62f1ed2417e8c9ffd44677f5b30fc9e476b9..f7c5ad5f38fae6fdb89487953fb486ae35e48ba0 100644
--- a/src/kernel_services/ast_queries/ast_info.ml
+++ b/src/kernel_services/ast_queries/ast_info.ml
@@ -39,7 +39,7 @@ let rec possible_value_of_integral_const = function
| _ -> None
and possible_value_of_integral_expr e =
- match (stripInfo e).enode with
+ match e.enode with
| Const c -> possible_value_of_integral_const c
| _ -> None
@@ -53,13 +53,13 @@ let value_of_integral_expr e =
| None -> assert false
| Some i -> i
-let rec is_null_expr e = match (stripInfo e).enode with
+let rec is_null_expr e = match e.enode with
| Const c when is_integral_const c ->
Integer.equal (value_of_integral_const c) Integer.zero
| CastE(_,e) -> is_null_expr e
| _ -> false
-let rec is_non_null_expr e = match (stripInfo e).enode with
+let rec is_non_null_expr e = match e.enode with
| Const c when is_integral_const c ->
not (Integer.equal (value_of_integral_const c) Integer.zero)
| CastE(_,e) -> is_non_null_expr e
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index e4e407d1b53294b1407b8543a8c85cbfc9e97ac2..db32e083853b0f47d2e51061cde25d9e19676f46 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -253,11 +253,6 @@ let find_default_requires behaviors =
try (List.find is_default_behavior behaviors).b_requires
with Not_found -> []
-let rec stripInfo e =
- match e.enode with
- | Info(e',_) -> stripInfo e'
- | _ -> e
-
let rec addOffset (toadd: offset) (off: offset) : offset =
match off with
| NoOffset -> toadd
@@ -2216,8 +2211,7 @@ and childrenExp (vis: cilVisitor) (e: exp) : exp =
let vTyp t = visitCilType vis t in
let vLval lv = visitCilLval vis lv in
let new_exp e' = { e with enode = e' } in
- match (stripInfo e).enode with
- | Info _ -> assert false
+ match e.enode with
| Const c ->
let c' = visitCilConst vis c in
if c' != c then new_exp (Const c') else e
@@ -3463,35 +3457,9 @@ let block_from_unspecified_sequence us =
let rec stripCasts (e: exp) =
match e.enode with CastE(_, e') -> stripCasts e' | _ -> e
-let rec stripCastsAndInfo (e: exp) =
- match e.enode with Info(e',_) | CastE(_,e') -> stripCastsAndInfo e' | _ -> e
-
-let rec stripCastsButLastInfo (e: exp) =
- match e.enode with
- Info({enode = (Info _ | CastE _)} as e',_)
- | CastE(_,e') ->
- stripCastsButLastInfo e'
- | _ -> e
-
let rec stripTermCasts (t: term) =
match t.term_node with TCastE(_, t') -> stripTermCasts t' | _ -> t
-let exp_info_of_term t = { exp_type = t.term_type; exp_name = t.term_name;}
-
-let term_of_exp_info loc tnode einfo =
- {
- term_node = tnode; term_loc = loc;
- term_type = einfo.exp_type; term_name = einfo.exp_name;
- }
-
-let map_under_info f e = match e.enode with
- | Info(e,einfo) -> new_exp ~loc:e.eloc (Info(f e,einfo))
- | _ -> f e
-
-let app_under_info f e = match e.enode with
- | Info(e,_) -> f e
- | _ -> f e
-
(* Separate out the storage-modifier name attributes *)
let separateStorageModifiers (al: attribute list) =
let isstoragemod (Attr(an, _) | AttrAnnot an : attribute) : bool =
@@ -3714,8 +3682,7 @@ let no_op_coerce typ t =
(**** Compute the type of an expression ****)
let rec typeOf (e: exp) : typ =
- match (stripInfo e).enode with
- | Info _ -> assert false
+ match e.enode with
| Const(CInt64 (_, ik, _)) -> TInt(ik, [])
(* Character constants have type int. ISO/IEC 9899:1999 (E),
@@ -4685,7 +4652,6 @@ and constFold (machdep: bool) (e: exp) : exp =
| Lval lv -> new_exp ~loc (Lval (constFoldLval machdep lv))
| AddrOf lv -> new_exp ~loc (AddrOf (constFoldLval machdep lv))
| StartOf lv -> new_exp ~loc (StartOf (constFoldLval machdep lv))
- | Info _ -> e (* Deprecated constructor *)
and constFoldLval machdep (host,offset) =
let newhost =
@@ -4753,8 +4719,6 @@ and constFoldBinOp ~loc (machdep: bool) bop e1 e2 tres =
when Integer.equal z Integer.zero -> e1''
| PlusPI, _, Const(CInt64(z,_,_))
when Integer.equal z Integer.zero -> e1''
- | IndexPI, _, Const(CInt64(z,_,_))
- when Integer.equal z Integer.zero -> e1''
| MinusPI, _, Const(CInt64(z,_,_))
when Integer.equal z Integer.zero -> e1''
| PlusA, Const(CInt64(i1,ik1,_)),Const(CInt64(i2,ik2,_)) when ik1 = ik2 ->
@@ -5813,8 +5777,7 @@ let isVariadicListType t = match unrollTypeSkel t with
| TBuiltin_va_list _ -> true
| _ -> false
-let rec isConstantGen f e = match (stripInfo e).enode with
- | Info _ -> assert false
+let rec isConstantGen f e = match e.enode with
| Const c -> f c
| UnOp (_, e, _) -> isConstantGen f e
| BinOp (_, e1, e2, _) -> isConstantGen f e1 && isConstantGen f e2
@@ -5953,7 +5916,7 @@ let mkBinOp ~loc op e1 e2 =
(mkCastT t1 t1' e1) (mkCastT t2 t2' e2) t1'
| (PlusA|MinusA)
when isArithmeticType t1 && isArithmeticType t2 -> doArithmetic ()
- | (PlusPI|MinusPI|IndexPI) when isPointerType t1 && isIntegralType t2 ->
+ | (PlusPI|MinusPI) when isPointerType t1 && isIntegralType t2 ->
constFoldBinOp ~loc machdep op e1 e2 t1
| MinusPP when isPointerType t1 && isPointerType t2 ->
(* NB: Same as cabs2cil. Check if this is really what the standard says*)
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index ebc091d0c73d33cbebd9b3ef0f88048ed2c3dc21..888fe0d6ff3ef9710e4f01768bde4ace9072c20f 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1015,28 +1015,6 @@ val stripTermCasts: term -> term
"(A)(B)(x + (C)y)", but leave the (C) cast. *)
val stripCasts: exp -> exp
-(** Removes info wrappers and return underlying expression *)
-val stripInfo: exp -> exp
-
-(** Removes casts and info wrappers and return underlying expression *)
-val stripCastsAndInfo: exp -> exp
-
-(** Removes casts and info wrappers,except last info wrapper, and return
- underlying expression *)
-val stripCastsButLastInfo: exp -> exp
-
-(** Extracts term information in an expression information *)
-val exp_info_of_term: term -> exp_info
-
-(** Constructs a term from a term node and an expression information *)
-val term_of_exp_info: location -> term_node -> exp_info -> term
-
-(** Map some function on underlying expression if Info or else on expression *)
-val map_under_info: (exp -> exp) -> exp -> exp
-
-(** Apply some function on underlying expression if Info or else on expression *)
-val app_under_info: (exp -> unit) -> exp -> unit
-
val typeOf: exp -> typ
(** Compute the type of an expression. *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index 6c438f5dd51da9fd580b0ae03731c1c1a586a0ac..ee6d4ef5573f305005e6e8ca321218f73bf56986 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1042,11 +1042,6 @@ struct
| AddrOf _, _ -> 1
| _, AddrOf _ -> -1
| StartOf lv1, StartOf lv2 -> compare_lval ~strict lv1 lv2
- | StartOf _, _ -> 1
- | _, StartOf _ -> -1
- | Info _, Info _ ->
- Cmdline.Kernel_log.fatal
- "[exp_compare] Info node is obsolete. Do not use it"
and compare_lval ~strict (h1,o1) (h2,o2) =
let res = compare_lhost ~strict h1 h2 in
@@ -1093,9 +1088,6 @@ struct
| CastE(ty,e) -> hash_exp ((prime*acc) lxor Typ.hash ty) e
| AddrOf lv -> hash_lval (prime*acc lxor 329) lv
| StartOf lv -> hash_lval (prime*acc lxor 431) lv
- | Info _ ->
- Cmdline.Kernel_log.fatal
- "Info node is deprecated and should not be used@."
and hash_lval acc (h,o) =
hash_offset ((prime * acc) lxor hash_lhost 856 h) o
and hash_lhost acc = function
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 69a4d9e33cb484fd8af1aacf3e1e9faebcf46fba..b2b63a486c0840c33b6eb25e45e7ec4f9e592474 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -1766,7 +1766,7 @@ struct
Logic_const.tat ~loc (add_offset lv here_idx,lab)
| _ ->
let b =
- { term_node = TBinOp (IndexPI, t, idx); term_name = [];
+ { term_node = TBinOp (PlusPI, t, idx); term_name = [];
term_loc = loc;
term_type = set_conversion t.term_type idx.term_type }
in
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index cde1a1284e89f4645fb5e8d221490ca2dea6562b..1b02633a34bbbb2319c376371285225ca8349465 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -33,7 +33,7 @@ val type_rel: Logic_ptree.relation -> Cil_types.relation
(** Arithmetic binop conversion. Addition and Subtraction are always
considered as being used on integers. It is the responsibility of the
- user to introduce PlusPI/IndexPI, MinusPI and MinusPP where needed.
+ user to introduce PlusPI, MinusPI and MinusPP where needed.
@since Nitrogen-20111001
*)
val type_binop: Logic_ptree.binop -> Cil_types.binop
diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml
index 4131258363e4c9061a648e697590d3f603aea9a3..d7e5d704db6d2a83a7466a157c835b1eb66b64e9 100644
--- a/src/kernel_services/ast_queries/logic_utils.ml
+++ b/src/kernel_services/ast_queries/logic_utils.ml
@@ -418,7 +418,7 @@ let is_boolean_binop op =
let open Cil_types in
match op with
| Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr -> true
- | PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP
+ | PlusA | PlusPI | MinusA | MinusPI | MinusPP
| Mult | Div | Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr -> false
let float_builtin prefix fkind =
@@ -505,9 +505,6 @@ let rec expr_to_term ?(coerce=false) e =
let coerce = Cil.isIntegralType (Cil.typeOf e) in
let t = mk_cast ~loc ty (expr_to_term ~coerce e) in
t.term_node , t.term_type
- | Info (e,_) ->
- let t = expr_to_term ~coerce e in
- t.term_node , t.term_type
in
let v = mk_cast ~loc typ @@ Logic_const.term ~loc node ltyp in
if coerce then
@@ -891,7 +888,7 @@ let is_same_pconstant c1 c2 =
let is_same_binop o1 o2 =
match o1,o2 with
| PlusA, PlusA
- | (PlusPI | IndexPI), (PlusPI | IndexPI) (* Semantically equivalent *)
+ | PlusPI, PlusPI
| MinusA, MinusA
| MinusPI, MinusPI
| MinusPP, MinusPP
@@ -912,7 +909,7 @@ let is_same_binop o1 o2 =
| LAnd, LAnd
| LOr, LOr ->
true
- | (PlusA | PlusPI | IndexPI | MinusA | MinusPI | MinusPP | Mult | Div
+ | (PlusA | PlusPI | MinusA | MinusPI | MinusPP | Mult | Div
| Mod | Shiftlt | Shiftrt | Cil_types.Lt | Cil_types.Gt | Cil_types.Le
| Cil_types.Ge | Cil_types.Eq | Cil_types.Ne
| BAnd | BXor | BOr | LAnd | LOr), _ ->
@@ -2529,7 +2526,7 @@ and constFoldBinOpToInt ~machdep bop e1 e2 =
match bop with
| PlusA -> Some (Integer.add i1 i2)
| MinusA -> Some (Integer.sub i1 i2)
- | PlusPI | IndexPI | MinusPI | MinusPP -> None
+ | PlusPI | MinusPI | MinusPP -> None
| Mult -> Some (Integer.mul i1 i2)
| Div ->
if Integer.(equal zero i2) && Integer.(is_zero (e_rem i1 i2)) then None
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index e46dd0eceea1402a7fb1445203ca096edf5c2a54..14d19b1b0859e3d71be9a323212c2af3d35c030d 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -851,13 +851,13 @@ let type_expr metaenv env ?tr ?current e =
&& Logic_typing.is_integral_type t2.term_type
then
Logic_const.term
- (TBinOp (IndexPI,t1,t2))
+ (TBinOp (PlusPI,t1,t2))
(Logic_typing.type_of_pointed t1.term_type)
else if Logic_utils.isLogicPointerType t2.term_type
&& Logic_typing.is_integral_type t1.term_type
then
Logic_const.term
- (TBinOp (IndexPI,t2,t1))
+ (TBinOp (PlusPI,t2,t1))
(Logic_typing.type_of_pointed t2.term_type)
else if Logic_utils.isLogicArrayType t1.term_type
&& Logic_typing.is_integral_type t2.term_type
diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 65c0a28875efff46b9dd1967ad788b95ce3a8cbd..472b894a5c219aca5ae41ba86c09b24baf3bd658 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -851,7 +851,6 @@ let rec infer t =
| Tlambda (_,_)
| TConst (LStr _ | LWStr _)
| TBinOp (PlusPI,_,_)
- | TBinOp (IndexPI,_,_)
| TBinOp (MinusPI,_,_)
| TAddrOf _
| TStartOf _
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 304ced042c78f899d15921da7e6190e9b37e994a..fcfc5c3d3bbdd49af3c9a7609cc68f75a15ecdff 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -221,13 +221,13 @@ module rec Transfer
(match lv with
| Var vi, _ -> Some vi
| Mem e, _ -> base_addr e)
- | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
+ | BinOp((PlusPI | MinusPI), e1, e2, _) ->
if is_ptr_or_array_exp e1 then base_addr e1
else begin
assert (is_ptr_or_array_exp e2);
base_addr e2
end
- | Info(e, _) | CastE(_, e) -> base_addr e
+ | CastE(_, e) -> base_addr e
| BinOp((MinusPP | PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt
| Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr),
_, _, _)
@@ -273,13 +273,13 @@ module rec Transfer
| AddrOf(lhost, _) ->
extend_to_expr true state lhost (Cil.new_exp ~loc:e.eloc (Lval lv)),
true
- | BinOp((PlusPI | IndexPI | MinusPI), e1, e2, _) ->
+ | BinOp((PlusPI | MinusPI), e1, e2, _) ->
if is_ptr_or_array_exp e1 then extend_from_addr state lv e1
else begin
assert (is_ptr_or_array_exp e2);
extend_from_addr state lv e2
end
- | CastE(_, e) | Info(e, _) -> extend_from_addr state lv e
+ | CastE(_, e) -> extend_from_addr state lv e
| _ -> state, false
let handle_assignment state (lhost, _ as lv) e =
@@ -314,7 +314,7 @@ module rec Transfer
| Tif(_, t1, t2) ->
let varinfos = register_term kf varinfos t1 in
register_term kf varinfos t2
- | TBinOp((PlusPI | IndexPI | MinusPI), t1, t2) ->
+ | TBinOp((PlusPI | MinusPI), t1, t2) ->
(match t1.term_type with
| Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t1
| _ ->
@@ -767,12 +767,12 @@ let rec apply_on_vi_base_from_lval f ?kf ?stmt = function
and apply_on_vi_base_from_exp f ?kf ?stmt e = match e.enode with
| Lval lv | AddrOf lv | StartOf lv ->
apply_on_vi_base_from_lval f ?kf ?stmt lv
- | BinOp((PlusPI | IndexPI | MinusPI), e1, _, _) ->
+ | BinOp((PlusPI | MinusPI), e1, _, _) ->
apply_on_vi_base_from_exp f ?kf ?stmt e1
| BinOp(MinusPP, e1, e2, _) ->
apply_on_vi_base_from_exp f ?kf ?stmt e1
|| apply_on_vi_base_from_exp f ?kf ?stmt e2
- | Info(e, _) | CastE(_, e) -> apply_on_vi_base_from_exp f ?kf ?stmt e
+ | CastE(_, e) -> apply_on_vi_base_from_exp f ?kf ?stmt e
| BinOp((PlusA | MinusA | Mult | Div | Mod |Shiftlt | Shiftrt | Lt | Gt | Le
| Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr), _, _, _)
| Const _ -> (* possible in case of static address *) false
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index bf14a866a21515dcb6b0ab59b90d2bdd7b55778c..8c949b9b18f6b3d79d9f7e40806a6d2fc107b9c4 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -543,7 +543,7 @@ let rec type_term
ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~lenv t);
dup Nan
- | TBinOp ((PlusPI | IndexPI | MinusPI), t1, t2) ->
+ | TBinOp ((PlusPI | MinusPI), t1, t2) ->
(* both [t1] and [t2] must be typed. *)
ignore (type_term ~use_gmp_opt:true ~ctx:Nan ~lenv t1);
let ctx = type_offset t2 in
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 2079c7e5ff2aa791d7ba89f81c8d40e07f849a1c..bda936cba38519ccb159ba03b09ad4ab6fef55c4 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -47,7 +47,7 @@ let name_of_mpz_arith_bop = function
| BXor -> "__gmpz_xor"
| Shiftlt -> "__gmpz_mul_2exp"
| Shiftrt -> "__gmpz_tdiv_q_2exp"
- | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | IndexPI | MinusPI
+ | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | MinusPI
| MinusPP as bop ->
Options.fatal
"Operation '%a' either not arithmetic or not supported on GMP integers"
diff --git a/src/plugins/e-acsl/src/code_generator/libc.ml b/src/plugins/e-acsl/src/code_generator/libc.ml
index 5c0ddb10d20bb8da524e10b46a61d333e88db513..8b55699909cd94b168f64d0ce40018663a991619 100644
--- a/src/plugins/e-acsl/src/code_generator/libc.ml
+++ b/src/plugins/e-acsl/src/code_generator/libc.ml
@@ -148,7 +148,7 @@ let zarith ~loc bop t1 t2 =
(* Check that we are building an arithmetic operation *)
(match bop with
| PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt -> ()
- | PlusPI | IndexPI | MinusPI | MinusPP | Lt | Gt | Le | Ge | Eq | Ne | BAnd
+ | PlusPI | MinusPI | MinusPP | Lt | Gt | Le | Ge | Eq | Ne | BAnd
| BXor | BOr | LAnd | LOr ->
Options.fatal
"Using Libc.zarith to build '%a' instead of an arithmetic operation"
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index db33c80d423bb876503ae0823ff0ffc9c0d48469..2b4c63c55e9bff22a29374bbde4c6fc22f004fae 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -487,7 +487,7 @@ let call_with_tset
if Misc.is_bitfield_pointers t.term_type then
Error.not_yet "bitfield pointer";
match t.term_node with
- | TBinOp((PlusPI | IndexPI),
+ | TBinOp(PlusPI,
ptr,
({ term_node = Trange _ } as r)) ->
if Misc.is_set_of_ptr_or_array ptr.term_type then
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 643823ebe1aa80e3c89d78e12fd682fbea180a71..17f633f25508e25c76b6e8026281030012882fea 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -223,7 +223,7 @@ let name_arith_bop = function
| Mult -> "__gmpq_mul"
| Div -> "__gmpq_div"
| Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
- | Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
+ | Shiftlt | Shiftrt | PlusPI | MinusPI | MinusPP -> assert false
let binop ~loc bop e1 e2 env kf t_opt =
let name = name_arith_bop bop in
diff --git a/src/plugins/e-acsl/src/code_generator/temporal.ml b/src/plugins/e-acsl/src/code_generator/temporal.ml
index ee153ec4791f2d117e6c91c560ce5d80da97a537..5964cc63f2a76c80a5004cc7832fe620dcbd70e0 100644
--- a/src/plugins/e-acsl/src/code_generator/temporal.ml
+++ b/src/plugins/e-acsl/src/code_generator/temporal.ml
@@ -182,7 +182,7 @@ let assign ?(ltype) lhs rhs loc =
base pointer and index so there should be no pointer arithmetic
operations there. The following bit is to make sure of it. *)
(match op with
- | MinusPI | PlusPI | IndexPI -> assert false
+ | MinusPI | PlusPI -> assert false
| _ -> ());
base, Direct
| _ -> assert false)
@@ -194,7 +194,7 @@ let assign ?(ltype) lhs rhs loc =
| AddrOf _ -> rhs
| Lval lv -> Cil.mkAddrOf ~loc lv
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
- | UnOp _ | BinOp _ | CastE _ | StartOf _ | Info _ ->
+ | UnOp _ | BinOp _ | CastE _ | StartOf _ ->
Options.abort "unsupported RHS %a" Printer.pp_exp rhs
in Some (lhs, rhs, Copy)
(* va_list is a builtin type, we assume it has no pointers here and treat
diff --git a/src/plugins/e-acsl/src/code_generator/translate_terms.ml b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
index 855400bbda51f71080f98de7caa86f88225575cb..3e03d9b22a4a31a3012051e1109c4822e548469f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate_terms.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate_terms.ml
@@ -694,7 +694,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
let e = Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)) in
e, adata, env, Typed_number.C_number, ""
end
- | TBinOp(PlusPI | IndexPI | MinusPI as bop, t1, t2) ->
+ | TBinOp(PlusPI | MinusPI as bop, t1, t2) ->
if Misc.is_set_of_ptr_or_array t1.term_type ||
Misc.is_set_of_ptr_or_array t2.term_type then
(* case of arithmetic over set of pointers (due to use of ranges)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index b39eb80446b5d3180f9552f94e586caab2a4a5be..17e737b66fe3578a7648efd7d32a5c3798ad0fe7 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -97,7 +97,7 @@ let rec ptr_base ~loc exp =
| BinOp(op, lhs, _, _) ->
(match op with
(* Pointer arithmetic: split pointer and integer parts *)
- | MinusPI | PlusPI | IndexPI -> ptr_base ~loc lhs
+ | MinusPI | PlusPI -> ptr_base ~loc lhs
(* Other arithmetic: treat the whole expression as pointer address *)
| MinusPP | PlusA | MinusA | Mult | Div | Mod
| BAnd | BXor | BOr | Shiftlt | Shiftrt
@@ -112,7 +112,6 @@ let rec ptr_base ~loc exp =
let exp, casts = strip_casts exp in
let base = ptr_base ~loc exp in
add_casts casts base
- | Info (exp, _) -> ptr_base ~loc exp
| Const _ | Lval _ | UnOp _ -> exp
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
-> assert false
@@ -211,7 +210,7 @@ let name_of_binop = function
| Mult -> "mul"
| PlusA -> "add"
| MinusA -> "sub"
- | MinusPP | MinusPI | IndexPI | PlusPI -> assert false
+ | MinusPP | MinusPI | PlusPI -> assert false
module Id_term =
Datatype.Make_with_collections
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index c28f33766a4107d7df9bdea8d498c8d166d60740..fe9417bc98ee3b8fd09979bdbb19b51a40f219b9 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -40,7 +40,6 @@ let rec find_deps_no_transitivity state expr =
(* The value of the expression [expr], just before executing the statement
[instr], is a function of the values of the returned zones. *)
match expr.enode with
- | Info (e, _) -> find_deps_no_transitivity state e
| AlignOfE _| AlignOf _| SizeOfStr _ |SizeOfE _| SizeOf _ | Const _
-> Function_Froms.Deps.bottom
| AddrOf lv | StartOf lv ->
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index 5c9705cb34e549d92a18a80ca50f77b53ef328c6..39a8827dd6a6ccf49727ac1b7cdb7a18c4d32dde 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -153,8 +153,6 @@ module Binary(* :BINARY_SEMILATTICE *) = struct
| BinOp(MinusA,e1,e2,_) ->
add (transfer_exp e1 load) (neg (transfer_exp e2 load))
| CastE(_,e) -> transfer_exp e load
- (* | BinOp((PlusPI|IndexPI|MinusA),_,_,_) -> assert false *)
- (* | BinOp(_,_,_,_) -> Unknown *)
| _ ->
(match Cil.constFoldToInt ~machdep:true exp with
| None -> Unknown
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 1f754dca975a8b6b243c72b451eca58d24a3f963..908ec80434e30091fc609a298ea8e5a7a7afd1e9 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -345,7 +345,6 @@ class annot_visitor kf flags on_alarm = object (self)
| StartOf _ | AddrOf _ ->
if self#do_pointer_value ()
then self#generate_assertion Rte.pointer_value exp
- | Info _
| UnOp _
| Const _
| BinOp _ -> ()
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index ae9be58a85904f013915c8555f84bdc20da5980b..02df6dedf82d0602cd775295e6e4a5edf5d48c00 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -267,7 +267,6 @@ let rec translate_expr eval oracle expr = match expr.enode with
Texpr1.(Binop (op', e1', e2', translate_typ typ, round))
| CastE (typ, e)->
coerce ~cast:true eval typ (translate_expr_linearize eval oracle e)
- | Info (e, _) -> translate_expr eval oracle e
| AddrOf _ | StartOf _ -> raise (Out_of_Scope "translate_expr addr")
| SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
match Cil.constFoldToInt expr with
diff --git a/src/plugins/value/domains/cvalue/builtins_split.ml b/src/plugins/value/domains/cvalue/builtins_split.ml
index 75e71fea2ebba821cb3358e22ab870da893fbf01..1b628c5876a293f554206e1ffe05906b7d8eab6f 100644
--- a/src/plugins/value/domains/cvalue/builtins_split.ml
+++ b/src/plugins/value/domains/cvalue/builtins_split.ml
@@ -129,7 +129,7 @@ let rec gather_lv_in_exp acc e =
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ ->
acc
| Lval lv | AddrOf lv | StartOf lv -> gather_lv_in_lv acc lv
- | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> gather_lv_in_exp acc e
+ | UnOp (_, e, _) | CastE (_, e) -> gather_lv_in_exp acc e
| BinOp (_, e1, e2, _) -> gather_lv_in_exp (gather_lv_in_exp acc e1) e2
and gather_lv_in_lv acc (host, offset as lv) =
let acc =
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index d6cf8037d451a216e86965fadc8ce4d612d3f09d..c51111bbd3f1a9f4c8f8806c203b9e4a15971928 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1019,13 +1019,12 @@ module G = struct
| BinOp (op, e1, e2, _) -> aux_binop (Cil.typeOf e) op e1 e2
- | Info _ -> assert false
and aux_binop typ_res op e1 e2 =
let g = match op with
| PlusA -> Gauge.add (aux e1) (aux e2)
| Mult -> Gauge.mul (aux e1) (aux e2)
| MinusA -> Gauge.sub (aux e1) (aux e2)
- | PlusPI | IndexPI ->
+ | PlusPI ->
Gauge.add (aux e1) (Gauge.mul_ct (ptr_size e1) (aux e2))
| MinusPI ->
Gauge.add (aux e1) (Gauge.neg (Gauge.mul_ct (ptr_size e1) (aux e2)))
diff --git a/src/plugins/value/domains/hcexprs.ml b/src/plugins/value/domains/hcexprs.ml
index 89c8ddc4839c37947a3910bd7bb58ae1728d0b33..71de08879f34c3415bd168aedcb211dd42d8d070 100644
--- a/src/plugins/value/domains/hcexprs.ml
+++ b/src/plugins/value/domains/hcexprs.ml
@@ -166,7 +166,7 @@ let syntactic_lvalues expr =
let new_lvalues = gather e empty_lvalues in
let new_addr = HCESet.union new_lvalues.read new_lvalues.addr in
{ lvalues with addr = HCESet.union new_addr lvalues.addr }
- | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> gather e lvalues
+ | UnOp (_, e, _) | CastE (_, e) -> gather e lvalues
| BinOp (_, e1, e2, _) -> gather e1 (gather e2 lvalues)
| _ -> lvalues
in
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index af0b45ea28f600470f52018c2dbfc441a71a5565..f44600a260c0819b362f33a4e16e58a5059e9484 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -260,8 +260,6 @@ module Rewriting = struct
if may_overflow ~cast:true typ v then [] else rewrite evaluate e
else []
- | Info (e, _) -> rewrite evaluate e
-
| _ -> []
(* Rewrites the operation [e1 ± e2] into equivalent octagons ±(X±Y-value). *)
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 0b797c95e5811bb54a7b01f5955bf7779990d847..b787c686b12e2763f8988d99d1d28ab7bee6a3dc 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -121,7 +121,7 @@ let interesting_exp get_locs get_val e =
match e.enode with
| Lval _ ->
not (Cvalue.V.cardinal_zero_or_one (get_val e))
- | CastE (_, e) | UnOp (_, e, _) | Info (e, _) ->
+ | CastE (_, e) | UnOp (_, e, _) ->
has_lvalue e
| BinOp (op, e1, e2,_) ->
not (is_comp op) && (has_lvalue e1 || has_lvalue e2)
@@ -134,7 +134,7 @@ let interesting_exp get_locs get_val e =
not (Precise_locs.cardinal_zero_or_one (get_locs lv))
| BinOp (op, e1, e2,_) ->
not (is_comp op) && has_lvalue e1 && has_lvalue e2
- | CastE _ | UnOp _ | Info _ | Const _ | SizeOf _ | SizeOfStr _ | SizeOfE _
+ | CastE _ | UnOp _ | Const _ | SizeOf _ | SizeOfStr _ | SizeOfE _
| AlignOf _ | AlignOfE _ | StartOf _ | AddrOf _ ->
false
@@ -145,7 +145,7 @@ and vars_exp (e: exp) = match e.enode with
Base.Set.empty
| AddrOf lv | StartOf lv | Lval lv ->
vars_lv lv
- | SizeOfE e | AlignOfE e | CastE (_,e) | UnOp (_,e,_) | Info (e,_) ->
+ | SizeOfE e | AlignOfE e | CastE (_,e) | UnOp (_,e,_) ->
vars_exp e
| BinOp (_,e1,e2,_) -> Base.Set.union (vars_exp e1) (vars_exp e2)
and vars_host = function
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 5cc270b5bac32da4c1bb76cc7366f35bf64f4d64..c194ece602cccce7dd801b1e183b30b32cb8c70f 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -421,7 +421,7 @@ module Make
| _ -> false
let may_overflow = function
- | Shiftlt | Mult | MinusPP | MinusPI | IndexPI | PlusPI
+ | Shiftlt | Mult | MinusPP | MinusPI | PlusPI
| PlusA | Div | Mod | MinusA -> true
| _ -> false
@@ -886,7 +886,6 @@ module Make
v, reduction, volatile
in
match expr.enode with
- | Info (e, _) -> internal_forward_eval context e
| Const constant -> internal_forward_eval_constant context expr constant
| Lval _lval -> assert false
@@ -1314,15 +1313,14 @@ module Make
Value.backward_cast ~src_typ ~dst_typ ~src_val ~dst_val:value
>>- function v -> backward_eval fuel state e v
end
- | Info (e, _) -> backward_eval fuel state e None
| _ -> `Value ()
and recursive_descent fuel state expr =
match expr.enode with
| Lval lval -> backward_lval fuel state lval
| UnOp (_, e, _)
- | CastE (_, e)
- | Info (e, _) -> backward_eval fuel state e None
+ | CastE (_, e) ->
+ backward_eval fuel state e None
| BinOp (_binop, e1, e2, _typ) ->
backward_eval fuel state e1 None >>- fun () ->
backward_eval fuel state e2 None
@@ -1490,8 +1488,8 @@ module Make
match expr.enode with
| Lval lval -> recursive_descent_lval state lval
| UnOp (_, e, _)
- | CastE (_, e)
- | Info (e, _) -> second_forward_eval state e
+ | CastE (_, e) ->
+ second_forward_eval state e
| BinOp (_binop, e1, e2, _typ) ->
second_forward_eval state e1 >>- fun () ->
second_forward_eval state e2
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 677b519020ead6dcc18e2ec04fc7fe039dccd42f..61a0a65264687d9a08090f372bfa90331d179aaa 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -98,7 +98,7 @@ let gather_non_linear expr =
if LvalMap.is_empty map && Cil.isArithmeticType (Cil.typeOfLval lv)
then LvalMap.singleton lv (expr, d, LvalSet.empty)
else map
- | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> compute depth e
+ | UnOp (_, e, _) | CastE (_, e) -> compute depth e
| BinOp (_, e1, e2, _) ->
(* Lvalues that appear in [e1] and [e2] are bound to [expr]. *)
let d = succ depth in union expr d (compute d e1) (compute d e2)
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 7a12a168d662e1d7225531415b317ba18e5bfbaf..38f26a2818715a2b85ce7be156e22ca79c1b1c36 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -150,8 +150,8 @@ let compute_englobing_subexpr ~subexpr ~expr =
else
let sublist = match expr.enode with
| UnOp (_, e, _)
- | CastE (_, e)
- | Info (e, _) -> compute e
+ | CastE (_, e) ->
+ compute e
| BinOp (_, e1, e2, _) ->
merge (compute e1) (compute e2)
| Lval (host, offset) ->
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 47f973535452ff86c1f4697ae0e8438bf2e903e9..c36e84a45b30286e18f983451fdff6d6a4171a81 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -535,7 +535,7 @@ let same_etype t1 t2 =
let infer_binop_res_type op targ =
match op with
| PlusA | MinusA | Mult | Div -> targ
- | PlusPI | MinusPI | IndexPI ->
+ | PlusPI | MinusPI ->
assert (Cil.isPointerType targ); targ
| MinusPP -> Cil.intType
| Mod | Shiftlt | Shiftrt | BAnd | BXor | BOr ->
@@ -1354,7 +1354,7 @@ and eval_binop ~alarm_mode env op t1 t2 =
int_or_float_op te1 (V.add_untyped_under ~factor) default
in
let eunder_op = match op with
- | PlusPI | IndexPI -> begin
+ | PlusPI -> begin
match Bit_utils.osizeof_pointed te1 with
| Int_Base.Top -> fun _ _ -> V.bottom
| Int_Base.Value _ as size -> add_untyped_op size
diff --git a/src/plugins/value/partitioning/auto_loop_unroll.ml b/src/plugins/value/partitioning/auto_loop_unroll.ml
index 199493025d1724e231988a6e7fe848f23d82e00a..8598544a9d4fa76c93009ab6510dce021fd3efeb 100644
--- a/src/plugins/value/partitioning/auto_loop_unroll.ml
+++ b/src/plugins/value/partitioning/auto_loop_unroll.ml
@@ -226,7 +226,7 @@ let classify eval_ptr loop_effect lval =
let rec is_const_expr expr =
match expr.enode with
| Lval lval -> classify_lval lval = Constant
- | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> is_const_expr e
+ | UnOp (_, e, _) | CastE (_, e) -> is_const_expr e
| BinOp (_, e1, e2, _) -> is_const_expr e1 && is_const_expr e2
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
| AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> true
@@ -262,7 +262,7 @@ let classify eval_ptr loop_effect lval =
let rec get_lvalues expr =
match expr.enode with
| Lval lval -> [ lval ]
- | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> get_lvalues e
+ | UnOp (_, e, _) | CastE (_, e) -> get_lvalues e
| BinOp (_op, e1, e2, _typ) -> get_lvalues e1 @ get_lvalues e2
| Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _
| AlignOf _ | AlignOfE _ | AddrOf _ | StartOf _ -> []
@@ -308,10 +308,9 @@ let transfer_assign lval exn f ~inner_loop acc instr =
let cross_equality loop lval =
(* If no such single equality can be found, return [lval] unchanged. *)
let exception No_equality in
- let rec find_lval expr x =
+ let find_lval expr _x =
match expr.enode with
| Lval lval -> lval
- | Info (e, _) -> find_lval e x
| _ -> raise No_equality
in
let transfer ~inner_loop lval instr =
@@ -367,7 +366,6 @@ module Make (Abstract: Abstractions.Eva) = struct
let rec is_lval e = match e.enode with
| Lval lv -> Cil_datatype.LvalStructEq.equal lval lv
| CastE (typ, e) -> Cil.isIntegralType typ && is_lval e
- | Info (e, _) -> is_lval e
| _ -> false
in
match Cil.constFoldToInt expr with
@@ -383,7 +381,6 @@ module Make (Abstract: Abstractions.Eva) = struct
then add_to_delta binop acc e1
else raise NoIncrement
| CastE (typ, e) when Cil.isIntegralType typ -> delta_assign lval e acc
- | Info (e, _) -> delta_assign lval e acc
| _ -> raise NoIncrement
(* Computes an over-approximation of the increment of [lval] in the [loop].
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 9d8b1c670b115a38ca2c74ef4f56001aaa153a9c..2e585515cff0920c414234bc28d18bad920f517f 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -206,7 +206,7 @@ let rec eval_deps state e =
| Lval lv -> eval_deps_lval state lv
| BinOp (_,e1,e2,_) ->
Locations.Zone.join (eval_deps state e1) (eval_deps state e2)
- | CastE (_,e) | UnOp (_,e,_) | Info (e,_) ->
+ | CastE (_,e) | UnOp (_,e,_) ->
eval_deps state e
| AddrOf lv | StartOf lv -> eval_deps_addr state lv
and eval_deps_lval state lv =
diff --git a/src/plugins/value/utils/eval_typ.ml b/src/plugins/value/utils/eval_typ.ml
index abbfccf9ed65c716e56277bce67fd825b4f43814..a84bbbbf5111d2a201997e3bc97cbdc62cbefd46 100644
--- a/src/plugins/value/utils/eval_typ.ml
+++ b/src/plugins/value/utils/eval_typ.ml
@@ -138,7 +138,7 @@ let compatible_functions typ_pointer ?args kfs =
let rec expr_contains_volatile expr =
let rec aux expr = match expr.enode with
| Lval lval -> lval_contains_volatile lval
- | UnOp (_, e, _) | CastE (_, e) | Info (e, _) -> aux e
+ | UnOp (_, e, _) | CastE (_, e) -> aux e
| AddrOf lv | StartOf lv -> lval_contains_volatile lv
| BinOp (_, e1, e2, _) -> aux e1 || aux e2
| _ -> false
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index 548a3cc8b12f85336c171ae26bb9230950b21623..cd0d402e1f9da9f64142f1ba106955cbc0b73b3c 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -280,7 +280,7 @@ let rec zone_of_expr find_loc expr =
| Lval lval ->
(* Dereference of an lvalue. *)
zone_of_lval find_loc lval
- | UnOp (_, e, _) | CastE (_, e) | Info (e, _) ->
+ | UnOp (_, e, _) | CastE (_, e) ->
(* Unary operators. *)
process e
| BinOp (_, e1, e2, _) ->
@@ -329,7 +329,7 @@ let rec height_expr expr =
match expr.enode with
| Const _ | SizeOf _ | SizeOfStr _ | AlignOf _ -> 0
| Lval lv | AddrOf lv | StartOf lv -> height_lval lv + 1
- | UnOp (_,e,_) | CastE (_, e) | Info (e,_) | SizeOfE e | AlignOfE e
+ | UnOp (_,e,_) | CastE (_, e) | SizeOfE e | AlignOfE e
-> height_expr e + 1
| BinOp (_,e1,e2,_) -> max (height_expr e1) (height_expr e2) + 1
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index 75db51158ff54761db2c5f4a34ccd7a5d75230f6..b124349d7b634f4038e1d7da6f9c3ca623254e9f 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -177,8 +177,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
match expr.enode with
| BinOp (Mod, _, modu, _typ) -> [modu]
| BinOp (BAnd, e1, e2, _typ) -> [e1; e2]
- | CastE (_, expr)
- | Info (expr, _) -> find_candidates expr
+ | CastE (_, expr) -> find_candidates expr
| _ -> []
in
let process expr =
diff --git a/src/plugins/value/values/cvalue_backward.ml b/src/plugins/value/values/cvalue_backward.ml
index 63d54e258d38fb1f4430e97f5435e076b62e3a03..889c776877859e26044a9b2aa40ea1c4b7d479c8 100644
--- a/src/plugins/value/values/cvalue_backward.ml
+++ b/src/plugins/value/values/cvalue_backward.ml
@@ -265,7 +265,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
| PlusA, TFloat (fk, _) -> backward_add_float (Fval.kind fk) ~res_value ~v1 ~v2 `Add
| MinusA, TFloat (fk, _) -> backward_add_float (Fval.kind fk) ~res_value ~v1 ~v2 `Sub
- | (PlusPI | IndexPI), TPtr _ -> backward_add_ptr typ ~res_value ~v1 ~v2 true
+ | PlusPI, TPtr _ -> backward_add_ptr typ ~res_value ~v1 ~v2 true
| MinusPI, TPtr _ -> backward_add_ptr typ ~res_value ~v1 ~v2 false
| MinusPP, TInt _ ->
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index aabd38688fe7f6f249672a86c0cfc8903a25c80b..1a3e65a3cc587a02bc1a96f1f968e678a6f4a434 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -376,8 +376,7 @@ let forward_minus_pp ~typ ev1 ev2 =
The function must behave as if it was acting on unbounded integers *)
let forward_binop_int ~typ ev1 op ev2 =
match op with
- | PlusPI
- | IndexPI -> V.add_untyped (Bit_utils.osizeof_pointed typ) ev1 ev2
+ | PlusPI -> V.add_untyped (Bit_utils.osizeof_pointed typ) ev1 ev2
| MinusPI ->
let int_base = Int_Base.neg (Bit_utils.osizeof_pointed typ) in
V.add_untyped int_base ev1 ev2
diff --git a/src/plugins/wp/CodeSemantics.ml b/src/plugins/wp/CodeSemantics.ml
index 0d3faf7370690d6520fe523710e6f9436d8563f4..d058aa8f72c4dd97e2b4588f2befe35b916baa3e 100644
--- a/src/plugins/wp/CodeSemantics.ml
+++ b/src/plugins/wp/CodeSemantics.ml
@@ -229,7 +229,7 @@ struct
| Ge -> Val (bool_of_comp env Cvalues.bool_leq M.loc_leq Cfloat.fle e2 e1)
| LAnd -> Val (Cvalues.bool_and (bool_of_exp env e1) (bool_of_exp env e2))
| LOr -> Val (Cvalues.bool_or (bool_of_exp env e1) (bool_of_exp env e2))
- | PlusPI | IndexPI ->
+ | PlusPI ->
let te = Cil.typeOf_pointed (Cil.typeOf e1) in
let obj = Ctypes.object_of te in
Loc(M.shift (loc_of_exp env e1) obj (val_of_exp env e2))
@@ -326,8 +326,6 @@ struct
| UnOp(op,e,ty) -> exp_unop env ty op e
| BinOp(op,e1,e2,tr) -> exp_binop env tr op e1 e2
- | Info(e,_) -> !s_exp env e
-
| AlignOfE _ | AlignOf _
| SizeOfE _ | SizeOf _ | SizeOfStr _ -> Val (Cvalues.constant_exp e)
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 06322b509861441f6af05e12df251c5162ce0a6d..f9ce31602dd9316b5099a6b4195c33053d7f4340 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -417,7 +417,7 @@ struct
| Mult -> arith env (L.apply e_mul) (L.apply F.e_mul) a b
| Div -> arith env (L.apply e_div) (L.apply F.e_div) a b
| Mod -> L.apply e_mod (C.logic env a) (C.logic env b)
- | PlusPI | IndexPI ->
+ | PlusPI ->
let va = C.logic env a in
let vb = C.logic env b in
let te = Logic_typing.ctype_of_pointed a.term_type in
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 560df2f561d6b89dec4b452815df43f21035c38a..44d5f5f5b44182122a62a4be701a673ac6673444 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -357,16 +357,13 @@ and expr (e:Cil_types.exp) : model = match e.enode with
(* Unary *)
| UnOp((Neg|BNot|LNot),e,_) -> mexpr e
- (* Jessie *)
- | Info(e,_) -> expr e
-
(* Binary *)
| BinOp( (MinusPP|PlusA|MinusA|Mult|Div|Mod
|Shiftlt|Shiftrt|BAnd|BXor|BOr|LAnd|LOr
|Lt|Gt|Le|Ge|Eq|Ne), a,b,_ ) -> m_vcup (expr a) (vexpr b)
(* Shifts *)
- | BinOp((PlusPI|IndexPI|MinusPI),a,b,_) -> shift (expr a) (vexpr b)
+ | BinOp((PlusPI|MinusPI),a,b,_) -> shift (expr a) (vexpr b)
(* Casts *)
| CastE(ty_tgt,e) -> cast (cast_ctyp ty_tgt (Cil.typeOf e)) (expr e)
@@ -419,7 +416,7 @@ and term (env:ctx) (t:term) : model = match t.term_node with
|Lt|Gt|Le|Ge|Eq|Ne), a,b ) -> m_vcup (term env a) (vterm env b)
(* Shifts *)
- | TBinOp((PlusPI|IndexPI|MinusPI),a,b) -> shift (term env a) (vterm env b)
+ | TBinOp((PlusPI|MinusPI),a,b) -> shift (term env a) (vterm env b)
(* Casts *)
| TCastE(ty_tgt,t) -> cast (cast_ltyp ty_tgt t.term_type) (term env t)
diff --git a/src/plugins/wp/RegionAccess.ml b/src/plugins/wp/RegionAccess.ml
index 066f2675a4006e361ce46442c7cde9ff09c492a4..2e47b7ade3a1489e1f8640d2bcbf45a4a8a0b910 100644
--- a/src/plugins/wp/RegionAccess.ml
+++ b/src/plugins/wp/RegionAccess.ml
@@ -121,7 +121,7 @@ let merge_addrof (map:map) v1 v2 =
let rec cc_exp (map:map) exp =
match exp.enode with
- | BinOp( (PlusPI | IndexPI | MinusPI) , a , b , _ ) ->
+ | BinOp( (PlusPI | MinusPI) , a , b , _ ) ->
cc_read map b ;
let { addrof = pointed } as addr = cc_addr map a in
acs_shift pointed (Eval exp) ;
@@ -134,7 +134,6 @@ let rec cc_exp (map:map) exp =
}
| Lval lv -> Read_at (Cil.typeOfLval lv , cc_lval map lv)
| CastE(ty,e) -> cast ty (cc_exp map e)
- | Info(e,_) -> cc_exp map e
| Const (CStr _ | CWStr _) -> Addr_of (cc_string map exp)
| Const (CInt64 _ | CChr _ | CEnum _ | CReal _)
| SizeOf _ | SizeOfE _ | SizeOfStr _
@@ -251,7 +250,7 @@ and cc_term_value (map:map) (term:term) =
shift = false ;
}
end
- | TBinOp( (PlusPI | IndexPI | MinusPI) , a , b ) ->
+ | TBinOp( (PlusPI | MinusPI) , a , b ) ->
begin
cc_term map b ;
let { addrof = pointed } as addr = cc_term_addr map a in
diff --git a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
index cb28e562b0c7e4b49a8ddd827e64c70298a7bd8a..d9212b184ab900e3b55fc458846461c422af1408 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle/reference_and_struct.res.oracle
@@ -260,7 +260,7 @@ Prove: true.
Memory model hypotheses for function 'call_reset_5_tps':
/*@
behavior wp_typed_ref:
- requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
+ requires \separated(tps[9] + (0 .. 4), (struct T **)tps + (..));
*/
void call_reset_5_tps(void);
[wp] reference_and_struct.i:88: Warning:
diff --git a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
index 078661743a9248acf5efce809e9077d94b9173bb..44907b868b9cc5538c94ed260c5ae73e7ea6d776 100644
--- a/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_hoare/oracle_qualif/reference_and_struct.res.oracle
@@ -58,7 +58,7 @@
Memory model hypotheses for function 'call_reset_5_tps':
/*@
behavior wp_typed_ref:
- requires \separated((struct T **)tps + (..), tps[9] + (0 .. 4));
+ requires \separated(tps[9] + (0 .. 4), (struct T **)tps + (..));
*/
void call_reset_5_tps(void);
[wp] reference_and_struct.i:88: Warning:
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 6bb11c8b6872cb7b46edebbd43548b4fe29b4d42..e9347956373a913c73e20a456495b8b6b4c06209 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -625,7 +625,7 @@ let rec term_hints hs t =
| TLval(lv,_) -> lval_hints hs lv
| TAddrOf(lv,_) -> lval_hints hs lv
| TCastE(_,t) -> term_hints hs t
- | TBinOp((PlusPI|IndexPI|MinusPI),a,_) -> term_hints hs a
+ | TBinOp((PlusPI|MinusPI),a,_) -> term_hints hs a
| Tlet(_,t) -> term_hints hs t
| _ -> ()
diff --git a/tests/libc/check_const.ml b/tests/libc/check_const.ml
index 3538cedcae139b2d99c4f48b283e9f548a5c67d7..710373708e0e41f8b386ecc4773030c6e56ba713 100644
--- a/tests/libc/check_const.ml
+++ b/tests/libc/check_const.ml
@@ -46,7 +46,7 @@ let check_annot kf _ (a: identified_predicate) =
warn typ vi t.term_loc
| _ -> ()
end
- | TBinOp ((PlusPI | MinusPI | IndexPI),
+ | TBinOp ((PlusPI | MinusPI),
({term_node = TLval (TVar lvi, _)} |
{term_node = TCastE (_, {term_node = TLval (TVar lvi, _)})}),
_)
diff --git a/tests/misc/interpreted_automata_dataflow_backward.ml b/tests/misc/interpreted_automata_dataflow_backward.ml
index be12ce941874d759193954a5f85e43fa013c111b..3642c0c878fa095cf8dfe227eecd724136d67f46 100644
--- a/tests/misc/interpreted_automata_dataflow_backward.ml
+++ b/tests/misc/interpreted_automata_dataflow_backward.ml
@@ -10,7 +10,7 @@ struct
let pretty fmt v =
Pretty_utils.pp_iter ~sep:",@ " Set.iter Cil_datatype.Varinfo.pretty fmt v
-
+
let join v1 v2 =
Set.union v1 v2
@@ -27,7 +27,7 @@ struct
| AlignOf _ | AlignOfE _
| AddrOf _ | StartOf _ ->
Set.empty
- | UnOp (_, e, _) | CastE (_,e) | Info (e,_) ->
+ | UnOp (_, e, _) | CastE (_,e) ->
vars e
| BinOp (_, e1, e2, _) ->
Set.union (vars e1) (vars e2)
@@ -37,7 +37,7 @@ struct
let transfer t v =
let open Interpreted_automata in
let r = match t with
- | Skip | Prop _ | Leave _ | Return (None,_) ->
+ | Skip | Prop _ | Leave _ | Return (None,_) ->
v (* Nothing to do *)
| Enter b ->
Set.diff v (Set.of_list b.blocals) (* If unconditionnaly initialized, they should not be there *)