package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val name : string

Used to create different datatypes each time the functor is applied

val default_offsetmap : Base.t -> Offsetmap.t Lattice_bounds.or_bottom

Value returned when a map is queried, and the base is not present. `Bottom indicates that the base is never bound in such a map.

val default_contents : V.t default_contents

This function is used to optimize functions that add keys in a map, in particular when maintaining canonicity w.r.t. default contents. It describes the contents c of the offsetmap resulting from default_offsetmap b. The possible values are:

  • Bottom means that c is V.bottom everywhere, and furthermore that V.bottom has an empty concretization. We deduce from this fact that unmapped keys do not contribute to a join, and that join c v is never c as soon as v is not itself v.
  • Top means that c is V.top everywhere. Thus unmapped keys have a default value more general than the one in a map where the key is bound.
  • `Constant v means that c is an offsetmap with a single interval containing v everywhere. v must be isotropic (in the sense of V.is_isotropic).
  • `Other means that default_offsetmap returns something arbitrary.

This function is only used on keys that change values. Thus it is safe to have default_offsetmap return something that do not match default_contents on constant keys.

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