functor (M : Memory.Model->
  sig
    type loc = M.loc
    type value = M.loc Memory.value
    type sigma = M.Sigma.t
    val print_value : Format.formatter -> M.loc Memory.value -> unit
    val cval : M.loc Memory.value -> Lang.F.term
    val cloc : M.loc Memory.value -> M.loc
    val is_zero_int : M.loc Memory.value -> Lang.F.pred
    val is_zero_float : M.loc Memory.value -> Lang.F.pred
    val is_zero_ptr : M.loc Memory.value -> Lang.F.pred
    val is_zero : M.sigma -> Ctypes.c_object -> M.loc -> Lang.F.pred
    val is_zero_range :
      M.sigma ->
      M.loc -> Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
    val s_exp :
      (CodeSemantics.Make.sigma -> Cil_types.exp -> CodeSemantics.Make.value)
      Pervasives.ref
    val s_cond :
      (CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.pred)
      Pervasives.ref
    val val_of_exp : CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.term
    val loc_of_exp : CodeSemantics.Make.sigma -> Cil_types.exp -> M.loc
    val loc_of_lhost : CodeSemantics.Make.sigma -> Cil_types.lhost -> M.loc
    val loc_of_offset :
      CodeSemantics.Make.sigma ->
      M.loc -> Cil_types.typ -> Cil_types.offset -> M.loc
    val lval :
      CodeSemantics.Make.sigma -> Cil_types.lhost * Cil_types.offset -> M.loc
    val exp_unop :
      CodeSemantics.Make.sigma ->
      Cil_types.typ -> Cil_types.unop -> Cil_types.exp -> 'Memory.value
    val arith :
      CodeSemantics.Make.sigma ->
      Cil_types.typ ->
      (Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term) ->
      (Ctypes.c_float -> Lang.F.term -> Lang.F.term -> Lang.F.term) ->
      Cil_types.exp -> Cil_types.exp -> 'Memory.value
    val arith_int :
      CodeSemantics.Make.sigma ->
      Cil_types.typ ->
      (Ctypes.c_int -> Lang.F.term -> Lang.F.term -> Lang.F.term) ->
      Cil_types.exp -> Cil_types.exp -> 'Memory.value
    val bool_of_comp :
      CodeSemantics.Make.sigma ->
      (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
      (M.loc -> M.loc -> Lang.F.pred) ->
      Cil_types.exp -> Cil_types.exp -> Lang.F.term
    val bool_of_exp :
      CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.term
    val exp_binop :
      CodeSemantics.Make.sigma ->
      Cil_types.typ ->
      Cil_types.binop -> Cil_types.exp -> Cil_types.exp -> M.loc Memory.value
    val cast :
      Cil_types.typ ->
      Cil_types.typ -> M.loc Memory.value -> M.loc Memory.value
    val exp_node :
      CodeSemantics.Make.sigma -> Cil_types.exp -> CodeSemantics.Make.value
    val call_node : CodeSemantics.Make.sigma -> Cil_types.exp -> M.loc
    val exp_handler : Cil_types.exp -> 'Memory.value
    val exp_protected :
      CodeSemantics.Make.sigma -> Cil_types.exp -> CodeSemantics.Make.value
    val equal_typ :
      Cil_types.typ ->
      M.loc Memory.value -> M.loc Memory.value -> Lang.F.pred
    val equal_obj :
      Ctypes.c_object ->
      M.loc Memory.value -> M.loc Memory.value -> Lang.F.pred
    val compare :
      CodeSemantics.Make.sigma ->
      (Lang.F.term -> Lang.F.term -> 'a) ->
      (M.loc -> M.loc -> 'a) -> Cil_types.exp -> Cil_types.exp -> 'a
    val cond_node : CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.pred
    val exp :
      CodeSemantics.Make.sigma -> Cil_types.exp -> CodeSemantics.Make.value
    val cond : CodeSemantics.Make.sigma -> Cil_types.exp -> Lang.F.pred
    val call : CodeSemantics.Make.sigma -> Cil_types.exp -> M.loc
    val return :
      CodeSemantics.Make.sigma ->
      Cil_types.typ -> Cil_types.exp -> Lang.F.term
    val instance_of : M.loc -> Kernel_function.t -> Lang.F.pred
  end