Frama-C API - Logic_infos
The analyses in Logic_normalizer may:
- create new auxiliary predicates and logic functions
- transform inductively and axiomatically defined logic functions and predicates into recursively defined ones This module provides functions to inquire about their status.
val generated_of : Frama_c_kernel.Cil_types.logic_info -> Frama_c_kernel.Cil_types.logic_info listauxiliary logic_infos generated from the given logic_info.
val origin_of_lv : Frama_c_kernel.Cil_types.logic_var -> Frama_c_kernel.Cil_types.logic_varIdentify the logic_info from which the logic_info identified by the given argument stems from. This is required in order to create meaningful feedback messages for the user who should not be confronted with the names of generated logic functions.