Frama-C:
Plug-ins:
Libraries:

Frama-C API - Transfer_stmt

type state = Dom.t
val assign : pos:Eva__.Position.t -> state -> Eva.Eval.lval -> Eva.Eval.exp -> state Eva.Eval.or_bottom
val assume : pos:Eva__.Position.t -> state -> Eva.Eval.exp -> bool -> state Eva.Eval.or_bottom
val call : pos:(Frama_c_kernel.Cil_types.stmt * Eva.Callstack.t) -> Eva.Eval.lval option -> Eva.Eval.lhost -> Eva.Eval.exp list -> state -> state Eva__.Engine_sig.call_result
val check_unspecified_sequence : pos:Eva__.Position.t -> state -> (Frama_c_kernel.Cil_types.stmt * Eva.Eval.lval list * Eva.Eval.lval list * Eva.Eval.lval list * Frama_c_kernel.Cil_types.stmt Stdlib.ref list) list -> unit Eva.Eval.or_bottom
val enter_scope : pos:Eva__.Position.t -> Frama_c_kernel.Cil_types.varinfo list -> state -> state