package frama-c

  1. Overview
  2. Docs

Module Interlang_gen.M

The intermediate language generation monad. It is used for translating E-ACSL predicates to expressions of the E-ACSL intermediate language (see Interlang).

include Monad_rws.S with type env = env and type state = state and type out = out
type env = env

Reader variable type

type out = out

Writer variable type

type state = state

State variable type

Standard monad functions and types

include Frama_c_kernel.Monad.S
type 'a t
val return : 'a -> 'a t
val flatten : 'a t t -> 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val bind : ('a -> 'b t) -> 'a t -> 'b t
module Bool : sig ... end

monadic convenience functions around booleans

module Option : sig ... end

applying monadic functions to the option type

module List : sig ... end

applying monadic functions to lists

module Operators : sig ... end
val run : env:env -> state:state -> 'a t -> 'a * out * state

execute state monad with initial environment env and initial state state

Reader monad

val read : env t

obtain the Reader value

val with_env : (env -> env) -> 'a t -> 'a t

run a sub-computation using a modified Reader value

Writer monad

val write : out -> unit t

send a value to the Writer side-channel

State monad

val get : state t

obtain the current value of the State variable

val set : state -> unit t

set a new value for the State variable

val modify : (state -> state) -> unit t

modify the current value of the State variable by applying a function

val not_covered : ?pre:string -> (Format.formatter -> 'a -> unit) -> 'a -> 'b t

The preferred method of raising the Not_covered exception. The format parameter should print the unsupported language element encountered. The ?pre parameter allows for some additional information to be printed alongside.

val read_logic_env : Analyses_datatype.Logic_env.t t

A convenience function to obtain the logic environment from the current Env.t-portion of the Reader variable.