package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val inline_calls : Cil_types.file -> unit
val inline_term : inline:(Cil_types.logic_info -> bool) -> ?current:Cil_types.logic_label -> Cil_types.term -> Cil_types.term option

inline_term ~inline term inlines in term the application of predicates and logic functions for which inline is true. If provided, current is the current label of the term; it is Here by default. Returns None if the inlining of a predicate or a logic function fails, in particular when they are recursive or have no direct definitiion.

val inline_predicate : inline:(Cil_types.logic_info -> bool) -> ?current:Cil_types.logic_label -> Cil_types.predicate -> Cil_types.predicate option

Inlines predicates and logic functions in a predicate. See inline_term for details.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct