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