Frama-C API - `Make`

Chunk Extension functor.

This functor promote an individual chunk type of some memory model into an uniform chunk.

Parameters

module C : ChunkType

type ckind +=

Chunk Extension.

val chunk : C.t -> chunk

Individual promotion of a model chunk to a uniform chunk.

val singleton : C.t -> domain

Promoted Domain.singleton.

val mem : sigma -> C.t -> bool

Specialized Sigma.mem, equivalent to Sigma.mem s (chunk c).

val get : sigma -> C.t -> F.var

Specialized Sigma.get, equivalent to Sigma.get s (chunk c).

val value : sigma -> C.t -> F.term

Specialized Sigma.value, equivalent to Sigma.value s (chunk c).