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:Position.t -> Frama_c_kernel.Cil_types.assigns -> state -> state
val compute_using_specification : warn:bool -> (location, value) Eval.call -> Frama_c_kernel.Cil_types.spec -> state -> (Partition.key * state) list