Inductive.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