Frama-C:
Plug-ins:
Libraries:

Frama-C API - Sigma

module F = Lang.F

Memory Environments.

The concrete memory is partionned into a vector of abstract data. Each component of the partition is called a memory chunk and holds an abstract representation of some part of the memory.

A sigma assigns a logical variable to each memory chunk, assigned lazily, that represents the contents of this slice of memory at a given program point.

Remark: memory chunks are not required to be independent from each other, provided the memory model implementation is consistent with the chosen representation. Conversely, a given object might be represented by several memory chunks.

type chunk

Memory chunk types.

The type of chunks is extensible. Each memory model extends this type with of its own memory chunks by functor Make.

type sigma

Memory chunks at a given program point.

This is a collection of variables indexed by chunks. New chunks are generated from the context pool of Lang.freshvar.

Chunks API

module type ChunkType = sig ... end
module Chunk : ChunkType with type t = chunk

Uniform access to chunks features.

module Heap : Qed.Collection.S with type t = chunk

Uniform Sets and Maps of chunks.

module Domain = Heap.Set
type domain = Domain.t

Memory footprint, ie. set of memory model chunk types.

type ckind = private ..

Internal representation of chunks (chunk-kind). This type can only be extended via functor Make.

val ckind : chunk -> ckind

Access to internal chunk representation.

module Make (C : ChunkType) : sig ... end

Chunk Extension functor.

Sigma API

val create : unit -> sigma

Initially empty environment.

val pretty : Stdlib.Format.formatter -> sigma -> unit

For debugging purpose

val mem : sigma -> chunk -> bool

Whether a chunk has been assigned.

val get : sigma -> chunk -> F.var

Lazily get the variable for a chunk.

val value : sigma -> chunk -> F.term

Same as Lang.F.e_var of get.

val copy : sigma -> sigma

Duplicate the environment. Fresh chunks in the copy are not duplicated into the source environment.

val join : sigma -> sigma -> Passive.t

Make two environment pairwise equal via the passive form.

Missing chunks in one environment are added with the corresponding variable of the other environment. When both environments don't agree on a chunk, their variables are added to the passive form.

val assigned : pre:sigma -> post:sigma -> domain -> F.pred Frama_c_kernel.Bag.t

Make chunks equal outside of some domain.

This is similar to join, but outside the given footprint of an assigns clause. Although, the function returns the equality predicates instead of a passive form.

Like in join, missing chunks are reported from one side to the other one, and common chunks are added to the equality bag.

val choose : sigma -> sigma -> sigma

Make the union of each sigma, choosing the minimal variable in case of conflict. Both initial environments are kept unchanged.

val merge : sigma -> sigma -> sigma * Passive.t * Passive.t

Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. Both initial environments are kept unchanged.

val merge_list : sigma list -> sigma * Passive.t list

Same than merge but for a list of sigmas. Much more efficient than folding merge step by step.

val iter : (chunk -> F.var -> unit) -> sigma -> unit

Iterates over the chunks and associated variables already accessed so far in the environment.

val iter2 : (chunk -> F.var option -> F.var option -> unit) -> sigma -> sigma -> unit

Same as iter for both environments.

val havoc_chunk : sigma -> chunk -> sigma

Generate a new fresh variable for the given chunk.

val havoc : sigma -> domain -> sigma

All the chunks in the provided footprint are generated and made fresh.

Existing chunk variables outside the footprint are copied into the new environment. The original environment itself is kept unchanged. More efficient than iterating havoc_chunk over the footprint.

val havoc_any : call:bool -> sigma -> sigma

All the chunks are made fresh. As an optimisation, when ~call:true is set, only non-local chunks are made fresh. Local chunks are those for which Chunk.is_frame returns true.

val remove_chunks : sigma -> domain -> sigma

Return a copy of the environment where chunks in the footprint have been removed. Keep the original environment unchanged.

val is_init : chunk -> bool

Shortcut to Chunk.is_init

val is_framed : chunk -> bool

Shortcut to Chunk.is_framed

val domain : sigma -> domain

Footprint of a memory environment. That is, the set of accessed chunks so far in the environment.

val union : domain -> domain -> domain

Same as Domain.union

val empty : domain

Same as Domain.empty

val writes : pre:sigma -> post:sigma -> domain

writes s indicates which chunks are new in s.post compared to s.pre.

type state = chunk F.Tmap.t
val state : sigma -> state
val apply : (F.term -> F.term) -> state -> state