package frama-c

  1. Overview
  2. Docs

Module Sigma.MakeSource

Chunk Extension functor.

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

Parameters

module C : ChunkType

Signature

Sourcetype ckind +=
  1. | Mu of C.t

Chunk Extension.

Sourceval chunk : C.t -> chunk

Individual promotion of a model chunk to a uniform chunk.

Sourceval singleton : C.t -> domain

Promoted Domain.singleton.

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

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

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

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

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

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