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
execute state monad with initial environment env
and initial state state
val not_covered :
?pre:string ->
(Stdlib.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.