Frama-C:
Plug-ins:
Libraries:

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.