Frama-C:
Plug-ins:
Libraries:

Frama-C API - Transfer_stmt

Interpretation of statements, built by functor Transfer_stmt.Make.

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