package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

Chunk Extension functor.

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

module C : ChunkType

Sourcetype ckind +=

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).

On This Page