diff --git a/src/kernel_services/ast_building/cil_builder.ml b/src/kernel_services/ast_building/cil_builder.ml
index 1ef5a124be602a5102c9e2257d1944de651f4aab..003b2f4bec284818318c46f880ff41eb6f4b0481 100644
--- a/src/kernel_services/ast_building/cil_builder.ml
+++ b/src/kernel_services/ast_building/cil_builder.ml
@@ -25,41 +25,63 @@
 
 module Type =
 struct
+  exception NotACType
+
   type ('value,'shape) morphology =
     | Single : ('value,'value) morphology
     | Listed : ('value,'shape) typ -> ('value,'shape list) morphology
 
-  and ('value,'shape) typ = ('value,'shape) morphology * Cil_types.typ
+  and ('value,'shape) typ = ('value,'shape) morphology * Cil_types.logic_type
 
   open Cil_types
 
-  let typ t = Single, t
-  let void = Single, TVoid []
-  let bool = Single, TInt (IBool, [])
-  let char = Single, TInt (IChar, [])
-  let schar = Single, TInt (ISChar, [])
-  let uchar = Single, TInt (IUChar, [])
-  let int = Single, TInt (IInt, [])
-  let unit = Single, TInt (IUInt, [])
-  let short = Single, TInt (IShort, [])
-  let ushort = Single, TInt (IUShort, [])
-  let long = Single, TInt (ILong, [])
-  let ulong = Single, TInt (IULong, [])
-  let longlong = Single, TInt (ILongLong, [])
-  let ulonglong = Single, TInt (IULongLong, [])
-  let float = Single, TFloat (FFloat, [])
-  let double = Single, TFloat (FDouble, [])
-  let longdouble = Single, TFloat (FLongDouble, [])
-
-  let ptr (_,t) = Single, TPtr (t, [])
-
-  let array ?size (_,t as typ) =
-    let size = Extlib.opt_map (Cil.integer ~loc:Cil_datatype.Location.unknown) size in
-    Listed typ,
-    TArray (t, size, Cil.empty_size_cache (), [])
+  (* Loggic types *)
+
+  let of_ltyp t = Single, t
+  let integer = Single, Linteger
+  let real = Single, Lreal
+
+  (* C base types *)
+
+  let of_ctyp t = Single, Ctype t
+  let void = Single, Ctype (TVoid [])
+  let bool = Single, Ctype (TInt (IBool, []))
+  let char = Single, Ctype (TInt (IChar, []))
+  let schar = Single, Ctype (TInt (ISChar, []))
+  let uchar = Single, Ctype (TInt (IUChar, []))
+  let int = Single, Ctype (TInt (IInt, []))
+  let unit = Single, Ctype (TInt (IUInt, []))
+  let short = Single, Ctype (TInt (IShort, []))
+  let ushort = Single, Ctype (TInt (IUShort, []))
+  let long = Single, Ctype (TInt (ILong, []))
+  let ulong = Single, Ctype (TInt (IULong, []))
+  let longlong = Single, Ctype (TInt (ILongLong, []))
+  let ulonglong = Single, Ctype (TInt (IULongLong, []))
+  let float = Single, Ctype (TFloat (FFloat, []))
+  let double = Single, Ctype (TFloat (FDouble, []))
+  let longdouble = Single, Ctype (TFloat (FLongDouble, []))
+
+  let ptr = function
+    | _, Ctype t -> Single, Ctype (TPtr (t, []))
+    | _, _ -> raise NotACType
+
+  let array ?size = function
+    | (_,Ctype t) as typ ->
+      let to_exp = Cil.integer ~loc:Cil_datatype.Location.unknown in
+      let size = Extlib.opt_map to_exp size in
+      Listed typ,
+      Ctype (TArray (t, size, Cil.empty_size_cache (), []))
+    | _, _ -> raise NotACType
+
+
+  (* Attrbutes *)
 
   let attribute (s,t) name params =
     let add_to = Cil.addAttribute (Attr (name, params)) in
+    let t = match t with
+      | Ctype t -> t
+      | _ -> raise NotACType
+    in
     let t = match t with
       | TVoid l -> TVoid (add_to l)
       | TInt (kind, l) -> TInt (kind, add_to l)
@@ -72,12 +94,19 @@ struct
       | TEnum (enuminfo, l) -> TEnum (enuminfo, add_to l)
       | TBuiltin_va_list l -> TBuiltin_va_list (add_to l)
     in
-    (s,t)
+    (s,Ctype t)
 
   let const typ = attribute typ "const" []
   let stdlib_generated typ = attribute typ "fc_stdlib_generated" []
 
-  let cil_typ (_,t) = t
+
+  (* Conversion *)
+
+  let cil_typ = function
+    | _, Ctype ty -> ty
+    | _, _ -> raise NotACType
+
+  let cil_logic_type (_,t) = t
 end
 
 
@@ -97,6 +126,8 @@ struct
     3. it is much easier to type the program with regular variants
   *)
 
+  type label = Cil_types.logic_label
+
   type const' =
     | Int of int
     | Integer of Integer.t
@@ -108,6 +139,7 @@ struct
     | Var of var'
     | Result
     | Mem of exp'
+    | Index of lval' * exp'
     | Field of lval' * Cil_types.fieldinfo
     | FieldNamed of lval' * string
   and exp' =
@@ -119,8 +151,19 @@ struct
     | Range of exp' option * exp' option
     | Unop of Cil_types.unop * exp'
     | Binop of Cil_types.binop * exp' * exp'
-    | Cast of Cil_types.typ * exp'
+    | Cast of Cil_types.logic_type * exp'
     | Addr of lval'
+    | App of Cil_types.logic_info * label list * exp' list
+    | Pred of pred'
+  and pred' =
+    | ObjectPointer of label * exp'
+    | Valid of label * exp'
+    | ValidRead of label * exp'
+    | Initialized of label * exp'
+    | Dangling of label * exp'
+    | Allocable of label * exp'
+    | Freeable of label * exp'
+    | Fresh of label * label * exp' * exp'
   and init' =
     | CilInit of Cil_types.init
     | SingleInit of exp'
@@ -132,6 +175,7 @@ struct
   type exp = [ const | lval | `exp of exp' ]
   type init = [ exp | `init of init']
 
+
   (* Depolymorphize *)
 
   let harden_const c =
@@ -169,17 +213,38 @@ struct
     | #exp as exp -> SingleInit (harden_exp exp)
     | `init init -> init
 
-  (* Build *)
 
-  let constant c = `const (CilConstant c)
-  let integer i = `const (Integer i)
-  let int i = `const (Int i)
-  let zero = int 0
-  let one = int 1
+  (* None *)
+
+  let none = `none
+
+  (* Labels *)
+
+  let here = Cil_types.(BuiltinLabel Here)
+  let old = Cil_types.(BuiltinLabel Old)
+  let pre = Cil_types.(BuiltinLabel Pre)
+  let post = Cil_types.(BuiltinLabel Post)
+  let loop_entry = Cil_types.(BuiltinLabel LoopEntry)
+  let loop_current = Cil_types.(BuiltinLabel LoopCurrent)
+  let program_init = Cil_types.(BuiltinLabel Init)
+
+  (* Constants *)
+
+  let of_constant c = `const (CilConstant c)
+  let of_integer i = `const (Integer i)
+  let of_int i = `const (Int i)
+  let zero = of_int 0
+  let one = of_int 1
+
+  (* Lvalules *)
+
   let var v = `var v
-  let lval lv = `lval (CilLval lv)
-  let exp e = `exp (CilExp e)
-  let exp_copy e = `exp (CilExpCopy e)
+  let of_lval lv = `lval (CilLval lv)
+
+  (* Expressions *)
+
+  let of_exp e = `exp (CilExp e)
+  let of_exp_copy e = `exp (CilExpCopy e)
   let unop op e = `exp (Unop (op, harden_exp e))
   let neg e = unop Cil_types.Neg e
   let lognot e = unop Cil_types.LNot e
@@ -187,7 +252,7 @@ struct
   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 e one
-  let add_int e i = add e (int i)
+  let add_int e i = add e (of_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
@@ -205,26 +270,15 @@ struct
   let bwxor e1 e2 = binop Cil_types.BXor e1 e2
   let logand e1 e2 = binop Cil_types.LAnd e1 e2
   let logor e1 e2 = binop Cil_types.LOr e1 e2
-  let cast' t e = `exp (Cast (t,harden_exp e))
-  let cast (_,t) e = cast' t e
+  let cast' t e = `exp (Cast (Cil_types.Ctype t, harden_exp e))
+  let cast (_,t) e = `exp (Cast (t, harden_exp e))
   let addr lv = `exp (Addr (harden_lval lv))
   let mem e = `lval (Mem (harden_exp e))
+  let index lv e = `lval (Index (harden_lval lv, harden_exp e))
   let field lv fi = `lval (Field (harden_lval lv, fi))
   let fieldnamed lv s = `lval (FieldNamed (harden_lval lv, s))
-  let result = `lval Result
-  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))
 
-  let rec values : type a. (init, a) typ -> a -> [> init] =
-    fun (morph,typ) x ->
-    match morph with
-    | Single -> x
-    | Listed sub -> compound typ (List.map (values sub) x)
+  (* Expression lists *)
 
   exception EmptyList
 
@@ -236,34 +290,64 @@ struct
   let logand_list l = reduce logand l
   let logor_list l = reduce logor l
 
+  (* Term specific *)
+
+  let result = `lval Result
+  let term t = `exp (CilTerm t)
+  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 app logic_info labels args =
+    `exp (App (logic_info, labels, harden_exp_list args))
+
+  let object_pointer ?(at=here) e =
+    `exp (Pred (ObjectPointer (at, harden_exp e)))
+  let valid ?(at=here) e = `exp (Pred (Valid (at, harden_exp e)))
+  let valid_read ?(at=here) e = `exp (Pred (ValidRead (at, harden_exp e)))
+  let initialized ?(at=here) e = `exp (Pred (Initialized (at, harden_exp e)))
+  let dangling ?(at=here) e = `exp (Pred (Dangling (at, harden_exp e)))
+  let allocable ?(at=here) e = `exp (Pred (Allocable (at, harden_exp e)))
+  let freeable ?(at=here) e = `exp (Pred (Freeable (at, harden_exp e)))
+  let fresh l1 l2 e1 e2 =
+    `exp (Pred (Fresh  (l1, l2, harden_exp e1, harden_exp e2)))
+
+  (* Initializations *)
+
+  let of_init i = `init (CilInit i)
+  let compound t l = `init (CompoundInit (t, List.map harden_init l))
+
+  let rec values : type a. (init, a) typ -> a -> [> init] =
+    fun ty x ->
+    match ty with
+    | Single, Ctype _ -> x
+    | Listed sub, Ctype t-> compound t (List.map (values sub) x)
+    | _, _ -> raise NotACType
+
+  (* Operators *)
+
   let (+), (-), ( * ), (/), (%) = add, sub, mul, div, modulo
   let (<<), (>>) = shiftl, shiftr
   let (<), (>), (<=), (>=), (==), (!=) = lt, gt, le, ge, eq, ne
+  let (--) = range
 
   (* Convert *)
 
-  exception LogicInC
-  exception CInLogic
+  exception LogicInC of exp
+  exception CInLogic of exp
+  exception NotATerm of exp
+  exception NotAPredicate of exp
+  exception NotAFunction of Cil_types.logic_info
   exception Typing_error of string
 
-  let get_fieldinfo typ fieldname =
-    match Cil.unrollType typ with
-    | Cil_types.TComp (compinfo,_,_) ->
-      begin try
-          Cil.getCompField compinfo fieldname
-        with Not_found ->
-          let cname = compinfo.Cil_types.cname in
-          raise (Typing_error ("no field " ^ fieldname ^ " in " ^ cname))
-      end
-    | _ ->
-      raise (Typing_error ("trying to get a field of a non-composite type"))
+  let typing_error s =
+    raise (Typing_error s)
+
+  let get_field ci s =
+    try
+      Cil.getCompField ci s
+    with Not_found ->
+      typing_error ("no field " ^ s ^ " in " ^ ci.Cil_types.cname)
 
-  let get_fieldinfo_from_ltype ltyp fieldname =
-    match Logic_utils.unroll_type ltyp with
-    | Cil_types.Ctype typ ->
-      get_fieldinfo typ fieldname
-    | _ ->
-      raise (Typing_error ("trying to get a field of a logic type"))
 
   let rec build_constant = function
     | CilConstant const -> const
@@ -271,24 +355,45 @@ struct
     | Integer i -> Cil_types.(CInt64 (i, IInt, None))
 
   and build_lval ~loc = function
+    | Result as lv -> raise (LogicInC (`lval lv))
     | CilLval lval -> lval
     | Var v -> Cil_types.(Var v, NoOffset)
-    | Result -> raise LogicInC
     | Mem e ->
-      Cil.mkMem ~addr:(build_exp ~loc e) ~off:Cil_types.NoOffset
-    | Field (lv,f) ->
-      let host, offset = build_lval ~loc lv in
-      let offset' = Cil.addOffset Cil_types.(Field (f, NoOffset)) in
-      host, offset' offset
-    | FieldNamed (lv,s) ->
-      let (host, offset) as lval = build_lval ~loc lv in
-      let ty = Cil.typeOfLval lval in
-      let f = get_fieldinfo ty s in
-      let offset' = Cil_types.(Field (f, NoOffset)) in
-      host, Cil.addOffset offset' offset
+      let e' = build_exp ~loc e in
+      Cil.mkMem ~addr:e' ~off:Cil_types.NoOffset
+    | Index (lv, e) ->
+      let (host, offset) as lv' = build_lval ~loc lv
+      and e' = build_exp ~loc e in
+      begin match Cil.(unrollType (typeOfLval lv')) with
+        | TArray _ ->
+          let offset' = Cil_types.Index (e', NoOffset) in
+          host, Cil.addOffset offset' offset
+        | TPtr _ ->
+          let base = Cil.new_exp ~loc (Lval lv') in
+          let addr = Cil.mkBinOp ~loc Cil_types.PlusPI base e' in
+          Cil.mkMem ~addr ~off:Cil_types.NoOffset
+        | _ -> typing_error "trying to index an lvalue which is not an array \
+                             or a pointer"
+      end
+    | (Field (lv,_) | FieldNamed (lv,_)) as e ->
+      let (host, offset) as lv' = build_lval ~loc lv in
+      let host', offset', ci = match Cil.(unrollTypeDeep (typeOfLval lv')) with
+        | TComp (ci,_,_) -> host, offset, ci
+        | TPtr (TComp (ci,_,_),_) ->
+          Mem (Cil.new_exp ~loc (Lval lv')), Cil_types.NoOffset, ci
+        | _ -> typing_error "trying to get a field of an lvalue which is not \
+                             of composite type or pointer to a composite type"
+      in
+      let f = match e with
+        | Field (_lv,f) -> f
+        | FieldNamed (_lv,s) -> get_field ci s
+        | _ -> assert false
+      in
+      let offset'' = Cil_types.(Field (f, NoOffset)) in
+      host', Cil.addOffset offset'' offset'
 
   and build_exp ~loc = function
-    | CilTerm _ | Range _ -> raise LogicInC
+    | CilTerm _ | Range _ | App _ | Pred _ as e -> raise (LogicInC (`exp e))
     | CilExp exp -> exp
     | CilExpCopy exp -> Cil.copy_exp exp
     | Const c->
@@ -314,29 +419,61 @@ struct
         | op -> op
       in
       Cil.mkBinOp ~loc op' e1' e2'
-    | Cast (newt, e) ->
+    | Cast (Cil_types.Ctype newt, e) ->
       Cil.mkCast ~force:false ~e:(build_exp ~loc e) ~newt
+    | Cast _ ->
+      raise NotACType
     | Addr lv ->
       Cil.mkAddrOrStartOf ~loc (build_lval ~loc lv)
 
   let rec build_term_lval ~loc ~restyp = function
-    | CilLval _ -> raise CInLogic
+    | Result -> Cil_types.(TResult (Extlib.the restyp), TNoOffset)
+    | CilLval _ as lv -> raise (CInLogic (`lval lv))
     | Var v -> Cil_types.(TVar (Cil.cvar_to_lvar v), TNoOffset)
-    | Mem e -> Cil_types.(TMem (build_term ~loc ~restyp e), TNoOffset)
-    | Result -> Cil_types.(TResult restyp, TNoOffset)
-    | Field (lv,f) ->
-      let host, offset = build_term_lval ~loc ~restyp lv in
-      let offset' = Cil_types.(TField (f, TNoOffset)) in
-      host, Logic_const.addTermOffset offset' offset
-    | FieldNamed (lv,s) ->
-      let (host, offset) as tlval = build_term_lval ~loc ~restyp lv in
-      let ty = Cil.typeOfTermLval tlval in
-      let f = get_fieldinfo_from_ltype ty s in
-      let offset' = Cil_types.(TField (f, TNoOffset)) in
-      host, Logic_const.addTermOffset offset' offset
+    | Mem t ->
+      let t' = build_term ~loc ~restyp t in
+      Cil_types.(TMem t', TNoOffset)
+    | Index (tlv, t) ->
+      let (host, offset) as tlv' = build_term_lval ~loc ~restyp tlv
+      and t' = build_term ~loc ~restyp t in
+      let lty = Cil.typeOfTermLval tlv' in
+      begin match Logic_utils.unroll_type lty with
+        | Ctype (TArray _) ->
+          let offset' = Cil_types.(TIndex (t', TNoOffset)) in
+          host, Logic_const.addTermOffset offset' offset
+        | Ctype (TPtr _) ->
+          let base = Logic_const.term ~loc (TLval tlv') lty in
+          let addr = Logic_const.term ~loc (TBinOp (PlusPI,base,t')) lty in
+          TMem addr, TNoOffset
+        | _ -> typing_error "trying to index a term lvalue which is not a C \
+                             array or a C pointer"
+      end
+    | (Field (tlv,_) | FieldNamed (tlv,_)) as t ->
+      let (host, offset) as tlv' = build_term_lval ~loc ~restyp tlv in
+      let lty = match Logic_utils.unroll_type (Cil.typeOfTermLval tlv') with
+        | Ctype cty -> Cil_types.Ctype (Cil.unrollTypeDeep cty)
+        | lty -> lty
+      in
+      let host', offset', ci = match lty with
+        | Ctype (TComp (ci,_,_)) -> host, offset, ci
+        | Ctype (TPtr (TComp (ci,_,_),_)) ->
+          TMem (Logic_const.term ~loc (Cil_types.TLval tlv') lty), TNoOffset, ci
+        | _ -> typing_error "trying to get a field of an lvalue which is not \
+                             of composite type or pointer to a composite type"
+      in
+      let f = match t with
+        | Field (_lv,f) -> f
+        | FieldNamed (_lv,s) -> get_field ci s
+        | _ -> assert false
+      in
+      let offset'' = Cil_types.(TField (f, TNoOffset)) in
+      host', Logic_const.addTermOffset offset'' offset'
 
   and build_term ~loc ~restyp = function
-    | Const (CilConstant _) | CilExp _ | CilExpCopy _ -> raise CInLogic
+    | Const (CilConstant _) | CilExp _ | CilExpCopy _ as e ->
+      raise (CInLogic (`exp e))
+    | Pred _ as e ->
+      raise (NotATerm (`exp e))
     | CilTerm term -> term
     | Const (Int i) ->
       Logic_const.tinteger ~loc i
@@ -354,11 +491,21 @@ struct
       let t1' = build_term ~loc ~restyp t1
       and t2' = build_term ~loc ~restyp t2 in
       let ty = t1'.Cil_types.term_type in
+      let op' = match op with (* Normalize operation *)
+        | PlusA when Logic_utils.isLogicPointer t1' -> Cil_types.PlusPI
+        | MinusA when Logic_utils.isLogicPointer t1' -> Cil_types.MinusPI
+        | PlusPI when not (Logic_utils.isLogicPointer t1') -> Cil_types.PlusA
+        | MinusPI when not (Logic_utils.isLogicPointer t1') -> Cil_types.MinusA
+        | op -> op
+      in
       (* TODO: type conversion *)
-      Logic_const.term ~loc Cil_types.(TBinOp (op,t1',t2')) ty
-    | Cast (ct, t) ->
+      Logic_const.term ~loc Cil_types.(TBinOp (op',t1',t2')) ty
+    | Cast (Ctype ct, t) ->
       let t' = build_term ~loc ~restyp t in
-      Logic_const.term ~loc Cil_types.(TCastE (ct, t')) (Ctype ct)
+      Logic_utils.mk_cast ~loc ct t'
+    | Cast (ty, t) ->
+      let t' = build_term ~loc ~restyp t in
+      Logic_utils.numeric_coerce ty t'
     | Addr lval ->
       let tlval = build_term_lval ~loc ~restyp lval in
       let ty = Cil.typeOfTermLval tlval in
@@ -367,6 +514,67 @@ struct
       let t1' = Extlib.opt_map (build_term ~loc ~restyp) t1
       and t2' = Extlib.opt_map (build_term ~loc ~restyp) t2 in
       Logic_const.trange ~loc (t1',t2')
+    | App (logic_info, labels, args) ->
+      let ty = match logic_info.l_type with
+        | None -> raise (NotAFunction logic_info)
+        | Some ty -> ty
+      in
+      let args' = List.map (build_term ~loc ~restyp) args in
+      Logic_const.term ~loc (Tapp (logic_info, labels, args')) ty
+
+  and build_relation e = function
+    | Cil_types.Lt -> Cil_types.Rlt
+    | Cil_types.Gt -> Cil_types.Rgt
+    | Cil_types.Le -> Cil_types.Rle
+    | Cil_types.Ge -> Cil_types.Rge
+    | Cil_types.Eq -> Cil_types.Req
+    | Cil_types.Ne -> Cil_types.Rneq
+    | _ -> raise (NotAPredicate (`exp e))
+
+  and build_pred_node ~loc ~restyp = function
+    | Unop (Cil_types.LNot, p) ->
+      let p' = build_pred ~loc ~restyp p in
+      Cil_types.Pnot p'
+    | Binop (Cil_types.LAnd, p1, p2) ->
+      let p1' = build_pred ~loc ~restyp p1
+      and p2' = build_pred ~loc ~restyp p2 in
+      Cil_types.Pand (p1',p2')
+    | Binop (Cil_types.LOr, p1, p2) ->
+      let p1' = build_pred ~loc ~restyp p1
+      and p2' = build_pred ~loc ~restyp p2 in
+      Cil_types.Por (p1',p2')
+    | Binop (binop, t1, t2) as e ->
+      let rel = build_relation e binop
+      and t1' = build_term ~loc ~restyp t1
+      and t2' = build_term ~loc ~restyp t2 in
+      Cil_types.Prel (rel, t1', t2')
+    | Const _ | CilExp _ | CilExpCopy _  | CilTerm _
+    | Lval _ | Unop _ | Cast _ | Addr _ | Range _ as e ->
+      raise (NotAPredicate (`exp e))
+    | App (logic_info, labels, args) ->
+      let args' = List.map (build_term ~loc ~restyp) args in
+      Cil_types.Papp (logic_info, labels, args')
+    | Pred (ObjectPointer (l, t)) ->
+      Cil_types.Pobject_pointer (l, build_term ~loc ~restyp t)
+    | Pred (Valid (l, t)) ->
+      Cil_types.Pvalid (l, build_term ~loc ~restyp t)
+    | Pred (ValidRead (l, t)) ->
+      Cil_types.Pvalid_read (l, build_term ~loc ~restyp t)
+    | Pred (Initialized (l, t)) ->
+      Cil_types.Pinitialized (l, build_term ~loc ~restyp t)
+    | Pred (Dangling (l, t)) ->
+      Cil_types.Pdangling (l, build_term ~loc ~restyp t)
+    | Pred (Allocable (l, t)) ->
+      Cil_types.Pallocable (l, build_term ~loc ~restyp t)
+    | Pred (Freeable (l, t)) ->
+      Cil_types.Pfreeable (l, build_term ~loc ~restyp t)
+    | Pred (Fresh (l1, l2, t1, t2)) ->
+      let t1' = build_term ~loc ~restyp t1
+      and t2' = build_term ~loc ~restyp t2 in
+      Cil_types.Pfresh (l1, l2, t1', t2')
+
+  and build_pred ~loc ~restyp t =
+    Logic_const.unamed ~loc (build_pred_node ~loc ~restyp t)
 
   let rec build_init ~loc = function
     | CilInit init -> init
@@ -380,6 +588,7 @@ struct
 
   (* Export *)
 
+  let cil_logic_label label = label
   let cil_varinfo v = harden_var v
   let cil_constant c = build_constant (harden_const c)
   let cil_lval ~loc lv = build_lval ~loc (harden_lval lv)
@@ -388,10 +597,17 @@ struct
   let cil_exp ~loc e = build_exp ~loc (harden_exp e)
   let cil_exp_opt ~loc e = Extlib.opt_map (build_exp ~loc) (harden_exp_opt e)
   let cil_exp_list ~loc l = List.map (cil_exp ~loc) l
-  let cil_term_lval ~loc ~restyp lv =
+  let cil_term_lval ~loc ?restyp lv =
     build_term_lval ~loc ~restyp (harden_lval lv)
-  let cil_term ~loc ~restyp e = build_term ~loc ~restyp (harden_exp e)
+  let cil_term ~loc ?restyp e = build_term ~loc ~restyp (harden_exp e)
+  let cil_iterm ~loc ?restyp e =
+    Logic_const.new_identified_term (cil_term ~loc ?restyp e)
+  let cil_pred ~loc ?restyp e = build_pred ~loc ~restyp (harden_exp e)
+  let cil_ipred ~loc ?restyp e =
+    Logic_const.new_predicate (cil_pred ~loc ?restyp e)
   let cil_init ~loc i = build_init ~loc (harden_init i)
+
+  let cil_typeof (`var vi) = vi.Cil_types.vtype
 end
 
 
@@ -441,16 +657,16 @@ struct
 
   (* Build *)
 
-  let instr i = `instr (CilInstr i)
+  let of_instr i = `instr (CilInstr i)
   let skip = `instr Skip
   let assign dest src = `instr (Assign (harden_lval dest, harden_exp src))
   let incr dest = `instr (Assign (harden_lval dest, harden_exp (add dest one)))
   let call res callee args =
     `instr (Call (harden_lval_opt res, harden_exp callee, harden_exp_list args))
 
-  let stmtkind sk = `stmt (CilStmtkind sk)
-  let stmt s = `stmt (CilStmt s)
-  let stmts l = `stmt (Sequence (List.map (fun s -> CilStmt s) l))
+  let of_stmtkind sk = `stmt (CilStmtkind sk)
+  let of_stmt s = `stmt (CilStmt s)
+  let of_stmts l = `stmt (Sequence (List.map (fun s -> CilStmt s) l))
   let block l = `stmt (Sequence (List.map harden_stmt l))
   let ghost s = `stmt (Ghost (harden_stmt s))
 
@@ -678,17 +894,26 @@ struct
 
   (* Statements *)
 
-  let stmt s =
+  let of_stmt s =
     let b = top () in
     append_stmt b (CilStmt s)
 
-  let stmts l =
-    List.iter stmt l
+  let of_stmts l =
+    List.iter of_stmt l
 
-  let stmtkind sk =
+  let of_stmtkind sk =
     let b = top () in
     append_stmt b (CilStmtkind sk)
 
+  let break () =
+    of_stmtkind (Cil_types.Break loc)
+
+  let return exp =
+    of_stmtkind (Cil_types.Return (cil_exp_opt ~loc exp, loc))
+
+
+  (* Blocks *)
+
   let new_block ?(ghost=false) scope_type = {
     scope_type;
     ghost;
@@ -696,9 +921,27 @@ struct
     vars = [];
   }
 
-  let open_function ?ghost name =
+  let extract_ifthen_block b =
+    match b.scope_type with
+    | IfThen {ifthen_exp} -> ifthen_exp
+    | _ -> raise (WrongContext "not in an opened if-then-else context")
+
+  let extract_switch_block b =
+    match b.scope_type with
+    | Switch {switch_exp} -> switch_exp
+    | _ -> raise (WrongContext "not in a opened switch context")
+
+  let extract_function_block b =
+    match b.scope_type with
+    | Function {fundec} -> fundec
+    | _ -> raise (WrongContext "not in a opened function context")
+
+  let open_function ?ghost ?vorig_name name =
     check_empty ();
-    let fundec = Cil.emptyFunction name in
+    let vorig_name = Extlib.opt_conv name vorig_name in
+    let fundec = Cil.emptyFunction vorig_name in
+    fundec.svar.vdecl <- loc;
+    fundec.svar.vname <- name;
     set_owner fundec;
     push (new_block ?ghost (Function {fundec}));
     `var fundec.Cil_types.svar
@@ -722,17 +965,14 @@ struct
 
   let open_else () =
     let b = pop () in
-    let ifthenelse_exp = match b.scope_type with
-      | IfThen {ifthen_exp} -> ifthen_exp
-      | _ -> raise (WrongContext "not in an opened if-then-else context")
-    in
+    let ifthenelse_exp = extract_ifthen_block b in
     let then_block = build_block b in
     push (new_block (IfThenElse {ifthenelse_exp; then_block}))
 
   let close () =
     let above = pop () in
     check_not_empty ();
-    stmtkind (build_stmtkind above) (* add the block to the parent *)
+    of_stmtkind (build_stmtkind above) (* add the block to the parent *)
 
   let finish_block () =
     let b = finish () in
@@ -747,7 +987,7 @@ struct
       | Some block, vars ->
         block.Cil_types.blocals <- List.rev vars @ block.Cil_types.blocals
       | None, _ :: _ ->
-        raise (WrongContext "a scope must be provide to insert local variables")
+        raise (WrongContext "a scope must be provided to insert local variables")
     end;
     build_instr_list b.stmts
 
@@ -757,41 +997,120 @@ struct
 
   let finish_function ?(register=true) () =
     let b = finish () in
-    match b.scope_type with
-    | Function {fundec} ->
-      let open Cil_types in
-      fundec.sbody <- build_block b;
-      fundec.svar.vdefined <- true;
-      fundec.svar.vghost <- b.ghost;
-      if register then begin
-        let funspec = Cil.empty_funspec () in
-        Globals.Functions.replace_by_definition funspec fundec loc;
-        let keepSwitch = Kernel.KeepSwitch.get () in
-        Cfg.prepareCFG ~keepSwitch fundec;
-        Cfg.cfgFun fundec;
-      end;
-      GFun (fundec,loc)
-    | _ -> raise (WrongContext "not in a opened function context")
+    let fundec = extract_function_block b in
+    let open Cil_types in
+    let vi = fundec.svar and spec = fundec.sspec in
+    fundec.sbody <- build_block b;
+    vi.vdefined <- true;
+    vi.vghost <- b.ghost;
+    if register then begin
+      Globals.Functions.replace_by_definition spec fundec loc;
+      let keepSwitch = Kernel.KeepSwitch.get () in
+      Cfg.prepareCFG ~keepSwitch fundec;
+      Cfg.cfgFun fundec;
+    end;
+    GFun (fundec,loc)
+
+  let finish_declaration ?(register=true) () =
+    let b = finish () in
+    let fundec = extract_function_block b in
+    let open Cil_types in
+    let vi = fundec.svar and spec = fundec.sspec in
+    if b.stmts <> [] then
+      raise (WrongContext "there must not be any built statements");
+    vi.vdefined <- false;
+    vi.vghost <- b.ghost;
+    if register then begin
+      Globals.Functions.replace_by_declaration spec vi loc;
+    end;
+    GFunDecl (spec, vi, loc)
 
   let case exp =
     let b = top () in
-    match b.scope_type with
-    | Switch _context ->
-      let label = Cil_types.Case (cil_exp ~loc exp, loc) in
-      append_stmt b (Label label)
-    | _ -> raise (WrongContext "no in a opened switch context")
+    let _ = extract_switch_block b in
+    let label = Cil_types.Case (cil_exp ~loc exp, loc) in
+    append_stmt b (Label label)
 
-  let break () =
-    stmtkind (Cil_types.Break loc)
 
-  let return exp =
-    stmtkind (Cil_types.Return (cil_exp_opt ~loc exp, loc))
+  (* Functions *)
 
-  (* Variables *)
+  let get_return_type () =
+    let fundec = get_owner () in
+    Cil.getReturnType fundec.svar.vtype
 
-  let return_type typ =
+  let set_return_type' ty =
     let fundec = get_owner () in
-    Cil.setReturnType fundec typ
+    Cil.setReturnType fundec ty
+
+  let set_return_type ty =
+    set_return_type' (cil_typ ty)
+
+  let add_attribute attr =
+    let fundec = get_owner () in
+    fundec.svar.vattr <- Cil.addAttribute attr fundec.svar.vattr
+
+  let add_new_attribute attr params =
+    add_attribute (Cil_types.Attr (attr, params))
+
+  let add_stdlib_generated () =
+    add_new_attribute "fc_stdlib_generated" []
+
+
+  (* Behaviors *)
+
+  let current_behavior () =
+    let b = top () in
+    let fundec = extract_function_block b in
+    match fundec.sspec.spec_behavior with
+    | [] ->
+      let default_behavior = Cil.mk_behavior () in
+      fundec.sspec.spec_behavior <- [default_behavior];
+      default_behavior
+    | bhv :: _ -> bhv
+
+  type source = [exp | `indirect of exp]
+
+  let indirect src =
+    match (src :> source ) with
+    | #exp as it | `indirect it -> `indirect it
+
+  let assigns dests sources =
+    let open Cil_types in
+    let b = current_behavior ()
+    and restyp = get_return_type () in
+    let map_source src =
+      match (src :> source) with
+      | #Exp.exp as e ->
+        cil_iterm ~loc ~restyp e
+      | `indirect e ->
+        let t = cil_term ~loc ~restyp e in
+        let t' = { t with term_name = "indirect" :: t.term_name } in
+        Logic_const.new_identified_term t'
+    and map_dest dst =
+      cil_iterm ~loc ~restyp dst
+    in
+    let dests' = List.map map_dest dests
+    and sources' = List.map map_source sources in
+    let previous = match b.b_assigns with
+      | WritesAny -> []
+      | Writes l -> l
+    and newones = List.map (fun dst -> dst, From sources') dests' in
+    b.b_assigns <- Writes (previous @ newones)
+
+  let requires pred =
+    let open Cil_types in
+    let b = current_behavior ()
+    and restyp = get_return_type () in
+    b.b_requires <- b.b_requires @ [cil_ipred ~loc ~restyp pred]
+
+  let ensures pred =
+    let open Cil_types in
+    let b = current_behavior ()
+    and restyp = get_return_type () in
+    b.b_post_cond <- b.b_post_cond @ [Normal, cil_ipred ~loc ~restyp pred]
+
+
+  (* Variables *)
 
   let local' ?(ghost=false) ?init typ name =
     let fundec = get_owner () and b = top () in
@@ -807,9 +1126,9 @@ struct
     append_local v;
     `var v
 
-  let local ?ghost ?init typ name =
-    let init = Extlib.opt_map (values typ) init in
-    local' ?ghost ?init (snd typ) name
+  let local ?ghost ?init ty name =
+    let init = Extlib.opt_map (values ty) init in
+    local' ?ghost ?init (cil_typ ty) name
 
   let local_copy ?(ghost=false) ?(suffix="_tmp") (`var vi) =
     let fundec = get_owner () and b = top () in
@@ -830,31 +1149,31 @@ struct
 
   (* Instructions *)
 
-  let instr i =
+  let of_instr i =
     let b = top () in
     append_instr b i
 
   let assign lval exp =
     let lval' = cil_lval ~loc lval
     and exp' = cil_exp ~loc exp in
-    instr (Cil_types.Set (lval', exp', loc))
+    of_instr (Cil_types.Set (lval', exp', loc))
 
   let incr lval =
-    assign lval (add lval (int 1))
+    assign lval (add lval (of_int 1))
 
   let call dest callee args =
     let dest' = cil_lval_opt ~loc dest
     and callee' = cil_exp ~loc callee
     and args' = cil_exp_list ~loc args in
-    instr (Cil_types.Call (dest', callee', args', loc))
+    of_instr (Cil_types.Call (dest', callee', args', loc))
 
   let pure exp =
     let exp' = cil_exp ~loc exp in
-    let `var v = local' (Cil.typeOf exp') "tmp" ~init:(Exp.exp exp') in
+    let `var v = local' (Cil.typeOf exp') "tmp" ~init:(Exp.of_exp exp') in
     v.vdescr <- Some (Format.asprintf "%a" !Cil.pp_exp_ref exp')
 
   let skip () =
-    instr (Cil_types.Skip (loc))
+    of_instr (Cil_types.Skip (loc))
 
 
   (* Operators *)
diff --git a/src/kernel_services/ast_building/cil_builder.mli b/src/kernel_services/ast_building/cil_builder.mli
index eb72f9f880dcd8858ff3f98bf85b6e7da0e4fd72..21718b422698fb1cb4315cdf7cc04f3480a10da7 100644
--- a/src/kernel_services/ast_building/cil_builder.mli
+++ b/src/kernel_services/ast_building/cil_builder.mli
@@ -29,9 +29,17 @@
 
 module Type :
 sig
+  exception NotACType
+
   type ('value,'shape) typ
 
-  val typ : Cil_types.typ -> ('v,'v) typ
+  (* Logic types *)
+  val of_ltyp : Cil_types.logic_type -> (unit,unit) typ
+  val integer : (unit,unit) typ
+  val real : (unit,unit) typ
+
+  (* C base types *)
+  val of_ctyp : Cil_types.typ -> ('v,'v) typ
   val void : ('v,'v) typ
   val bool : ('v,'v) typ
   val char : ('v,'v) typ
@@ -52,12 +60,15 @@ sig
   val ptr : ('v,'s) typ -> ('v,'v) typ
   val array : ?size:int -> ('v,'s) typ -> ('v,'s list) typ
 
+  (* Attrbutes *)
   val attribute : ('v,'s) typ -> string -> Cil_types.attrparam list
     -> ('v,'s) typ
   val const : ('v,'s) typ -> ('v,'s) typ
   val stdlib_generated : ('v,'s) typ -> ('v,'s) typ
 
+  (* Conversion *)
   val cil_typ : ('v,'s) typ -> Cil_types.typ
+  val cil_logic_type : ('v,'s) typ -> Cil_types.logic_type
 end
 
 
@@ -73,29 +84,44 @@ sig
   type exp'
   type init'
 
+  type label
   type const = [ `const of const' ]
   type var = [ `var of var' ]
   type lval = [  var | `lval of lval' ]
   type exp = [ const | lval | `exp of exp' ]
   type init = [ exp | `init of init']
 
-  (* Build Constants *)
+  val none : [> `none]
+
+  (* Labels *)
+
+  val here : label
+  val old : label
+  val pre : label
+  val post : label
+  val loop_entry : label
+  val loop_current : label
+  val program_init : label
 
-  val constant : Cil_types.constant -> [> const]
-  val int : int -> [> const]
-  val integer : Integer.t -> [> const]
+  (* Constants *)
+
+  val of_constant : Cil_types.constant -> [> const]
+  val of_int : int -> [> const]
+  val of_integer : Integer.t -> [> const]
   val zero : [> const]
   val one : [> const]
 
-  (* Build LValues *)
+  (* LValues *)
 
   val var : Cil_types.varinfo -> [> var]
-  val lval : Cil_types.lval -> [> lval]
+  val of_lval : Cil_types.lval -> [> lval]
+
+  (* Expressions *)
 
-  (* Build Expressions *)
+  exception EmptyList
 
-  val exp : Cil_types.exp -> [> exp]
-  val exp_copy : Cil_types.exp -> [> exp]
+  val of_exp : Cil_types.exp -> [> exp]
+  val of_exp_copy : Cil_types.exp -> [> exp]
   val unop : Cil_types.unop -> [< exp] -> [> exp]
   val neg : [< exp] -> [> exp]
   val lognot : [< exp] -> [> exp]
@@ -118,6 +144,8 @@ sig
   val ne : [< exp] -> [< exp] -> [> exp]
   val logor : [< exp] -> [< exp] -> [> exp]
   val logand : [< exp] -> [< exp] -> [> exp]
+  val logor_list : [< exp] list -> exp
+  val logand_list : [< exp] list -> exp
   val bwand : [< exp] -> [< exp] -> [> exp]
   val bwor : [< exp] -> [< exp] -> [> exp]
   val bwxor : [< exp] -> [< exp] -> [> exp]
@@ -125,22 +153,30 @@ sig
   val cast' : Cil_types.typ -> [< exp] -> [> exp]
   val addr : [< lval] -> [> exp]
   val mem : [< exp] -> [> lval]
+  val index : [< lval] -> [< exp] -> [> lval]
   val field : [< lval] -> Cil_types.fieldinfo -> [> lval]
   val fieldnamed : [< lval] -> string -> [> lval]
+
   val result : [> lval]
   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 app : Cil_types.logic_info -> label list -> [< exp] list -> [> exp]
+
+  val object_pointer : ?at:label -> [< exp] -> [> exp]
+  val valid : ?at:label -> [< exp] -> [> exp]
+  val valid_read : ?at:label -> [< exp] -> [> exp]
+  val initialized : ?at:label -> [< exp] -> [> exp]
+  val dangling : ?at:label -> [< exp] -> [> exp]
+  val allocable : ?at:label -> [< exp] -> [> exp]
+  val freeable : ?at:label -> [< exp] -> [> exp]
+  val fresh : label -> label -> [< exp] -> [< exp] -> [> exp]
+
+  val of_init : Cil_types.init -> [> init]
   val compound : Cil_types.typ -> init list -> [> init]
   val values : (init,'values) typ -> 'values -> init
 
-  exception EmptyList
-
-  val logor_list : [< exp] list -> exp
-  val logand_list : [< exp] list -> exp
 
   (* Redefined operators *)
 
@@ -157,22 +193,35 @@ sig
   val (>=) : [< exp] -> [< exp] -> [> exp]
   val (==) : [< exp] -> [< exp] -> [> exp]
   val (!=) : [< exp] -> [< exp] -> [> exp]
+  val (--) : [< exp] -> [< exp] -> [> exp]
 
   (* Export CIL objects from built expressions *)
 
-  exception LogicInC
-  exception CInLogic
+  exception LogicInC of exp
+  exception CInLogic of exp
+  exception NotATerm of exp
+  exception NotAPredicate of exp
+  exception NotAFunction of Cil_types.logic_info
   exception Typing_error of string
 
+  val cil_logic_label : label -> Cil_types.logic_label
   val cil_constant : [< const] -> Cil_types.constant
   val cil_varinfo : [< var] -> Cil_types.varinfo
   val cil_lval : loc:Cil_types.location -> [< lval] -> Cil_types.lval
   val cil_exp : loc:Cil_types.location -> [< exp] -> Cil_types.exp
-  val cil_term_lval : loc:Cil_types.location -> restyp:Cil_types.typ ->
+  val cil_term_lval : loc:Cil_types.location -> ?restyp:Cil_types.typ ->
     [< lval] -> Cil_types.term_lval
-  val cil_term : loc:Cil_types.location -> restyp:Cil_types.typ ->
+  val cil_term : loc:Cil_types.location -> ?restyp:Cil_types.typ ->
     [< exp] -> Cil_types.term
+  val cil_iterm : loc:Cil_types.location -> ?restyp:Cil_types.typ ->
+    [< exp] -> Cil_types.identified_term
+  val cil_pred : loc:Cil_types.location -> ?restyp:Cil_types.typ ->
+    [< exp] -> Cil_types.predicate
+  val cil_ipred : loc:Cil_types.location -> ?restyp:Cil_types.typ ->
+    [< exp] -> Cil_types.identified_predicate
   val cil_init : loc:Cil_types.location -> [< init] -> Cil_types.init
+
+  val cil_typeof : [< var] -> Cil_types.typ
 end
 
 
@@ -189,16 +238,16 @@ sig
   type stmt = [ instr | `stmt of stmt' ]
 
   (* Instructions *)
-  val instr : Cil_types.instr -> [> instr]
+  val of_instr : Cil_types.instr -> [> instr]
   val skip : [> instr]
   val assign : [< lval] -> [< exp] -> [> instr]
   val incr : [< lval] -> [> instr]
   val call : [< lval | `none] -> [< exp] -> [< exp] list -> [> instr]
 
   (* Statements *)
-  val stmtkind : Cil_types.stmtkind -> [> stmt]
-  val stmt : Cil_types.stmt -> [> stmt]
-  val stmts : Cil_types.stmt list -> [> stmt]
+  val of_stmtkind : Cil_types.stmtkind -> [> stmt]
+  val of_stmt : Cil_types.stmt -> [> stmt]
+  val of_stmts : Cil_types.stmt list -> [> stmt]
   val block : [< stmt] list -> [> stmt]
   val ghost : [< stmt] -> [> stmt]
 
@@ -226,11 +275,27 @@ module Stateful (Location : T) :
 sig
   include module type of Exp
 
+  (* Functions *)
+  val open_function : ?ghost:bool -> ?vorig_name:string -> string -> [> var]
+  val set_return_type : ('s,'v) typ -> unit
+  val set_return_type' : Cil_types.typ -> unit
+  val add_attribute : Cil_types.attribute -> unit
+  val add_new_attribute : string -> Cil_types.attrparam list -> unit
+  val add_stdlib_generated : unit -> unit
+  val finish_function : ?register:bool -> unit -> Cil_types.global
+  val finish_declaration : ?register:bool -> unit -> Cil_types.global
+
+  (* Behaviors *)
+  type source = [exp | `indirect of exp]
+  val indirect: [< source] -> [> source]
+  val assigns: [< exp] list -> [< exp | `indirect of [< exp]] list -> unit
+  val requires: [< exp] -> unit
+  val ensures: [< exp] -> unit
+
   (* Statements *)
-  val stmtkind : Cil_types.stmtkind -> unit
-  val stmt : Cil_types.stmt -> unit
-  val stmts : Cil_types.stmt list -> unit
-  val open_function : ?ghost:bool -> string -> [> var]
+  val of_stmtkind : Cil_types.stmtkind -> unit
+  val of_stmt : Cil_types.stmt -> unit
+  val of_stmts : Cil_types.stmt list -> unit
   val open_block : ?into:Cil_types.fundec -> ?ghost:bool -> unit -> unit
   val open_ghost : ?into:Cil_types.fundec -> unit -> unit
   val open_switch : ?into:Cil_types.fundec -> [< exp] -> unit
@@ -240,27 +305,25 @@ sig
   val finish_block : unit -> Cil_types.block
   val finish_instr_list : ?scope:Cil_types.block -> unit -> Cil_types.instr list
   val finish_stmt : unit -> Cil_types.stmt
-  val finish_function : ?register:bool -> unit -> Cil_types.global
   val case : [< exp] -> unit
   val break : unit -> unit
   val return : [< exp | `none] -> unit
 
-  (* Instructions *)
-  val instr : Cil_types.instr -> unit
-  val skip : unit -> unit
-  val assign : [< lval] -> [< exp] -> unit
-  val incr : [< lval] -> unit
-  val call : [< lval | `none] -> [< exp] -> [< exp] list -> unit
-  val pure : [< exp ] -> unit
-
   (* Variables *)
-  val return_type : Cil_types.typ -> unit
   val local : ?ghost:bool -> ?init:'v -> (init,'v) typ -> string -> [> var]
   val local' : ?ghost:bool -> ?init:init -> Cil_types.typ -> string -> [> var]
   val local_copy : ?ghost:bool -> ?suffix:string -> [< var] -> [> var]
   val parameter : ?ghost:bool -> ?attributes:Cil_types.attributes ->
     Cil_types.typ -> string -> [> var]
 
+  (* Instructions *)
+  val of_instr : Cil_types.instr -> unit
+  val skip : unit -> unit
+  val assign : [< lval] -> [< exp] -> unit
+  val incr : [< lval] -> unit
+  val call : [< lval | `none] -> [< exp] -> [< exp] list -> unit
+  val pure : [< exp ] -> unit
+
   (* Operators *)
   val (:=) : [< lval] -> [< exp] -> unit (* assign *)
   val (+=) : [< lval] -> [< exp] -> unit