MemoryContext (frama-c-wp.Wp.MemoryContext)

type validity =

type param =

val pp_param : Stdlib.Format.formatter -> param -> unit

type partition

val empty : partition

val set : Frama_c_kernel.Cil_types.varinfo -> param -> partition -> partition

val compute : 
  string ->
  (Frama_c_kernel.Cil_types.kernel_function -> partition) ->
  unit

val add_behavior : 
  Frama_c_kernel.Cil_types.kernel_function ->
  string ->
  (Frama_c_kernel.Cil_types.kernel_function -> partition) ->
  unit

val warn : 
  Frama_c_kernel.Cil_types.kernel_function ->
  string ->
  (Frama_c_kernel.Cil_types.kernel_function -> partition) ->
  unit