Frama-C:
Plug-ins:
Libraries:

Frama-C API - Transfer_specification

type value = Val.t
type location = Loc.location
type state = Dom.t
val treat_statement_assigns : pos:Eva__.Position.t -> Frama_c_kernel.Cil_types.assigns -> state -> state
val compute_using_specification : warn:bool -> (location, value) Eva.Eval.call -> Frama_c_kernel.Cil_types.spec -> state -> (Eva__.Partition.key * state) list