package frama-c

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Imperative environment to perform the fixpoint algorithm for recursive functions

find the currently inferred interval for a call to a logic function

val clear : unit -> unit

clear the table of intervals for logic function (to do between typing ) each logic function calls

add an interval as the current one for a logic function call

add 0..1 as the current interval for a predicate call

determine whether a logic function or predicate is recursive

replace the current interval for a logic function call