package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

logic environment: interval of all bound variables. It consists in two components

  • a profile for variables bound through function arguments
  • an association list for variables bound by a let or a quantification
type t

forward reference to meet of intervals

add a new binding for a let or a quantification binder only

val empty : t

the empty environment

val make : Profile.t -> t

create a new environment from a profile, for function calls

find a logic variable in the environment

val get_profile : t -> Profile.t

get the profile of the logic environment, i.e. bindings through function arguments

refine the interval of a logic variable: replace an interval with a more precise one