Frama-C:
Plug-ins:
Libraries:

Frama-C API - Inductive

This module transforms inductive predicate definitions into "direct" predicate definitions (introduced by LBpred), a form that can then be translated into Cil. It is in general not clear how inductive definitions can be translated into an executable form. However for a restricted set of inductive definitions this can be achieved. This subset is constituted of generalized Horn clauses, described in the reference manual under the subsection Inductive predicates.

exception Unsupported

This exception is raised if an inductive definition is not of a form that can be transformed into an executable form.

module Derived_functions : sig ... end

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.

transform a logic_info containing an inductively defined predicate (LBinductive) into a "directly" defined predicated (LBpred).

val clear : unit -> unit

clear memoization of inductives

val is_inductive : Frama_c_kernel.Cil_types.logic_info -> bool
  • returns

    true if logic_info contains an inductive definition

val is_fallthrough_term : Frama_c_kernel.Cil_types.term -> bool

For incomplete inductive definitions, it may happen that none of the constructors applies. In this case a fallthrough term is generated which is to be translated into a failing assertion. This function tests for terms being fallthrough terms.