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

type validity =

| Valid

| Nullable

type param =

| NotUsed

| ByAddr

| ByValue

| ByShift

| ByRef

| InContext of validity

| InArray of validity

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