Frama-C API - Sigma
Model Environments.
type chunk = Chunk.t
The type of memory chunks.
module Chunk = Heap
type domain = Chunk.Set.t
Memory footprint.
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
.
val pretty : Stdlib.Format.formatter -> t -> unit
For debugging purpose
val create : unit -> t
Initially empty environment.
val get : t -> chunk -> Lang.F.var
Lazily get the variable for a chunk.
val value : t -> chunk -> Lang.F.term
Same as Lang.F.e_var
of get
.
Duplicate the environment. Fresh chunks in the copy are not duplicated into the source environment.
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: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.
Make the union of each sigma, choosing the minimal variable in case of conflict. Both initial environments are kept unchanged.
Make the union of each sigma, choosing a new variable for each conflict, and returns the corresponding joins. Both initial environments are kept unchanged.
Same than merge
but for a list of sigmas. Much more efficient than folding merge step by step.
val iter : (chunk -> Lang.F.var -> unit) -> t -> unit
Iterates over the chunks and associated variables already accessed so far in the environment.
val iter2 : (chunk -> Lang.F.var option -> Lang.F.var option -> unit) -> t -> t -> unit
Same as iter
for both environments.
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.
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
.
Return a copy of the environment where chunks in the footprint have been removed. Keep the original environment unchanged.
Footprint of a memory environment. That is, the set of accessed chunks so far in the environment.
val empty : domain
Same as Chunk.Set.empty