Frama-C API - Derived_functions
extract_predicate
may generate auxiliary logic functions. Such a logic function f is stored in an hash table of this module table with the predicate p (from which f has been derived) as a key and f as a value. There may be multiple logic functions associated with a predicate.
val iter : (Frama_c_kernel.Cil_types.logic_info -> Frama_c_kernel.Cil_types.logic_info -> unit) -> unit