Frama-C API - `Make`

create an RWS monad from specification C

module type of an RWS monad

Parameters

module C : Conf

type env = C.env

Reader variable type

type out = C.out

Writer variable type

type state = C.state

State variable type

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

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

val write : out -> unit t

send a value to the Writer side-channel

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