sig
  type validity = Valid | Nullable
  type param =
      NotUsed
    | ByAddr
    | ByValue
    | ByShift
    | ByRef
    | InContext of Wp.MemoryContext.validity
    | InArray of Wp.MemoryContext.validity
  val pp_param : Stdlib.Format.formatter -> Wp.MemoryContext.param -> unit
  type partition
  val empty : Wp.MemoryContext.partition
  val set :
    Cil_types.varinfo ->
    Wp.MemoryContext.param ->
    Wp.MemoryContext.partition -> Wp.MemoryContext.partition
  val compute :
    string ->
    (Cil_types.kernel_function -> Wp.MemoryContext.partition) -> unit
  val add_behavior :
    Cil_types.kernel_function ->
    string ->
    (Cil_types.kernel_function -> Wp.MemoryContext.partition) -> unit
  val warn :
    Cil_types.kernel_function ->
    string ->
    (Cil_types.kernel_function -> Wp.MemoryContext.partition) -> unit
end