functor (M : Memory.Model->
  sig
    type loc = M.loc
    type value = Wp.CodeSemantics.Make.loc Wp.Memory.value
    type sigma = M.Sigma.t
    val cval : Wp.CodeSemantics.Make.value -> Wp.Lang.F.term
    val cloc : Wp.CodeSemantics.Make.value -> Wp.CodeSemantics.Make.loc
    val cast :
      Cil_types.typ ->
      Cil_types.typ ->
      Wp.CodeSemantics.Make.value -> Wp.CodeSemantics.Make.value
    val equal_typ :
      Cil_types.typ ->
      Wp.CodeSemantics.Make.value ->
      Wp.CodeSemantics.Make.value -> Wp.Lang.F.pred
    val equal_obj :
      Wp.Ctypes.c_object ->
      Wp.CodeSemantics.Make.value ->
      Wp.CodeSemantics.Make.value -> Wp.Lang.F.pred
    val exp :
      Wp.CodeSemantics.Make.sigma ->
      Cil_types.exp -> Wp.CodeSemantics.Make.value
    val cond : Wp.CodeSemantics.Make.sigma -> Cil_types.exp -> Wp.Lang.F.pred
    val lval :
      Wp.CodeSemantics.Make.sigma ->
      Cil_types.lval -> Wp.CodeSemantics.Make.loc
    val call :
      Wp.CodeSemantics.Make.sigma ->
      Cil_types.exp -> Wp.CodeSemantics.Make.loc
    val loc_of_exp :
      Wp.CodeSemantics.Make.sigma ->
      Cil_types.exp -> Wp.CodeSemantics.Make.loc
    val val_of_exp :
      Wp.CodeSemantics.Make.sigma -> Cil_types.exp -> Wp.Lang.F.term
    val return :
      Wp.CodeSemantics.Make.sigma ->
      Cil_types.typ -> Cil_types.exp -> Wp.Lang.F.term
    val is_zero :
      Wp.CodeSemantics.Make.sigma ->
      Wp.Ctypes.c_object -> Wp.CodeSemantics.Make.loc -> Wp.Lang.F.pred
    val is_exp_range :
      Wp.CodeSemantics.Make.sigma ->
      Wp.CodeSemantics.Make.loc ->
      Wp.Ctypes.c_object ->
      Wp.Lang.F.term ->
      Wp.Lang.F.term -> Wp.CodeSemantics.Make.value option -> Wp.Lang.F.pred
    val instance_of :
      Wp.CodeSemantics.Make.loc ->
      Cil_types.kernel_function -> Wp.Lang.F.pred
  end