Frama-C API - `Transfer_specification`

Interpretation of function specification, built by functor Transfer_specification.Make.

type value

type location

type state

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

Frama-C API - Transfer_specification