package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wp.SigmaSource

Sourcemodule 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 independant 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.

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

Sourcetype 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

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

Uniform access to chunks features.

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

Uniform Sets and Maps of chunks.

Sourcemodule Domain = Heap.Set
Sourcetype domain = Domain.t

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

Sourcetype ckind = private ..

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

Sourceval ckind : chunk -> ckind

Access to internal chunk representation.

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

Chunk Extension functor.

Sigma API

Sourceval create : unit -> sigma

Initially empty environment.

Sourceval pretty : Format.formatter -> sigma -> unit

For debugging purpose

Sourceval mem : sigma -> chunk -> bool

Whether a chunk has been assigned.

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

Lazily get the variable for a chunk.

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

Same as Lang.F.e_var of get.

Sourceval copy : sigma -> sigma

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

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

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

Sourceval choose : sigma -> sigma -> sigma

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

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

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

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

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

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

Same as iter for both environments.

Sourceval havoc_chunk : sigma -> chunk -> sigma

Generate a new fresh variable for the given chunk.

Sourceval 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 environement itself is kept unchanged. More efficient than iterating havoc_chunk over the footprint.

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

Sourceval remove_chunks : sigma -> domain -> sigma

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

Sourceval is_init : chunk -> bool

Shortcut to Chunk.is_init

Sourceval is_framed : chunk -> bool

Shortcut to Chunk.is_framed

Sourceval domain : sigma -> domain

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

Sourceval union : domain -> domain -> domain

Same as Domain.union

Sourceval empty : domain

Same as Domain.empty

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

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

Sourcetype state = chunk F.Tmap.t
Sourceval state : sigma -> state
Sourceval apply : (F.term -> F.term) -> state -> state
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct