package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Imperative environment to perform fixpoint algorithm for recursive functions. This environnement store four pieces of information associated to every logic_info:

  • the current profile in which the interval for the logic_info is infered.
  • the current interval that it is infered to.
  • a map associating to each parameter all the arguments in their profiles that this parameter has been called with up until now.
  • the depth of calls to the fixpoint algorithm associated to the logic_info. When this depth reaches 0, the entry corresponding to the logic_info is cleared thus avoiding unification between two independent calls to the same logic function, which is unsafe.

The third argument is used so that whenever a parameter of a logic_info is unified by widening with a new value, the interval inference algorithm updates all the arguments that this parameter have been called with, to assign the new interval to it

find the current profile in which a recursive function or predicate is being infered

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

return the pair of both the results of find_profile and find_ival

find all the arguments a recursive function or predicate has been called with

val clear : unit -> unit

clear the table of intervals for logic function

add ival as the current one for a logic function or predicate call

decrease the counter of fixpoint depth

update the current interval for the a given logic_info

determine whether a logic function or predicate is recursive