package frama-c

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

Module MemEmpty.SigmaSource

Model Environments.

Sourcetype chunk = Chunk.t

The type of memory chunks.

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

Memory footprint.

Sourcetype t

Environment assigning logic variables to chunk.

Memory chunk variables are assigned lazily. Hence, the vector is empty unless a chunk is accessed. Pay attention to this when you merge or havoc chunks.

New chunks are generated from the context pool of Lang.freshvar.

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

For debugging purpose

Sourceval create : unit -> t

Initially empty environment.

Sourceval mem : t -> chunk -> bool

Whether a chunk has been assigned.

Sourceval get : t -> chunk -> Lang.F.var

Lazily get the variable for a chunk.

Sourceval value : t -> chunk -> Lang.F.term

Same as Lang.F.e_var of get.

Sourceval copy : t -> t

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

Sourceval join : t -> t -> 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:t -> post:t -> domain -> Lang.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 : t -> t -> t

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

Sourceval merge : t -> t -> t * 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 : t list -> t * Passive.t list

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

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

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

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

Same as iter for both environments.

Sourceval havoc_chunk : t -> chunk -> t

Generate a new fresh variable for the given chunk.

Sourceval havoc : t -> domain -> t

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 -> t -> t

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 : t -> domain -> t

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

Sourceval domain : t -> 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 Chunk.Set.union

Sourceval empty : domain

Same as Chunk.Set.empty

Sourceval writes : t Sigs.sequence -> domain

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

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