package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-31.0-Gallium.tar.gz

sha256=a94384f00d53791cbb4b4d83ab41607bc71962d42461f02d71116c4ff6dca567

doc/frama-c-e-acsl.core/E_ACSL/Inductive/index.html

Module `E_ACSL.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.

val extract_predicate : 
  Frama_c_kernel.Cil_types.logic_info ->
  Frama_c_kernel.Cil_types.logic_info

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

raises Unsupported

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.