diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index 8af8b529e617e59e15bf98a38b79fb90eaa89651..836a84016ee29c5727166521fbc5339ee5dfd2e4 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -184,6 +184,8 @@ struct
   let bwnot e = unop Cil_types.BNot e
   let binop op e1 e2 = `exp (Binop (op, harden_exp e1, harden_exp e2))
   let add e1 e2 = binop Cil_types.PlusA e1 e2
+  let succ e = add e1 one
+  let increment e i = add e1 (int i)
   let sub e1 e2 = binop Cil_types.MinusA e1 e2
   let mul e1 e2 = binop Cil_types.Mult e1 e2
   let div e1 e2 = binop Cil_types.Div e1 e2
@@ -208,6 +210,8 @@ struct
   let term t = `exp (CilTerm t)
   let none = `none
   let range e1 e2 = `exp (Range (harden_exp_opt e1, harden_exp_opt e2))
+  let whole = `exp (Range (None, None))
+  let whole_right = `exp (Range (Some (Const (Int 0)), None))
   let init i = `init (CilInit i)
   let compound t l = `init (CompoundInit (t, List.map harden_init l))
 
@@ -294,7 +298,13 @@ struct
     | Binop (op,e1,e2) ->
       let e1' = build_exp ~loc e1
       and e2' = build_exp ~loc e2 in
-      Cil.mkBinOp ~loc op e1' e2'
+      let op' = match op with (* Normalize operation *)
+        | PlusA when Cil.isPointerType e1' -> PlusPI
+        | MinusA when Cil.isPointerType e1' -> MinusPI
+        | PlusPI when not Cil.isPointerType e1' -> PlusA
+        | MinusPI when not Cil.isPointerType e1' -> MinusA
+      in
+      Cil.mkBinOp ~loc op' e1' e2'
 
   let rec build_term_lval ~loc ~restyp = function
     | CilLval _ -> raise CInLogic
diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli
index af6de9843f91210d8880c20638531ea117bcadcd..f5c06677372d5faeb50bede71c6112a99860b92d 100644
--- a/src/kernel_services/ast_building/cil_builder.mli
+++ b/src/kernel_services/ast_building/cil_builder.mli
@@ -100,6 +100,8 @@ sig
   val neg : [< exp] -> [> exp]
   val lognot : [< exp] -> [> exp]
   val bwnot : [< exp] -> [> exp]
+  val succ : [< exp] -> [> exp] (* e + 1 *)
+  val increment : [< exp] -> int -> [> exp] (* e + i *)
   val binop : Cil_types.binop -> [< exp] -> [< exp] -> [> exp]
   val add : [< exp] -> [< exp] -> [> exp]
   val sub : [< exp] -> [< exp] -> [> exp]
@@ -126,6 +128,8 @@ sig
   val term : Cil_types.term -> [> exp]
   val none : [> `none]
   val range :  [< exp | `none] -> [< exp | `none] -> [> exp]
+  val whole : [> exp] (* Whole range, i.e. .. *)
+  val whole_right : [> exp] (* Whole range right side, i.e. 0.. *)
   val init : Cil_types.init -> [> init]
   val compound : Cil_types.typ -> init list -> [> init]
   val values : (init,'values) typ -> 'values -> init