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.kernel/Frama_c_kernel/Interpreted_automata/UnrollUnnatural/WTO/index.html

Module `UnrollUnnatural.WTO`

type node = vertex

type pref = node -> node -> int

Partial order of preference for the choice of the head of a loop. pref current_head new_candidate must return < 0 if new_candidate is preferred to current_head. Use "(fun _ _ -> 0)" for no specific preference.

val partition : 
  pref:pref ->
  init:node ->
  succs:(node -> node list) ->
  node Wto.partition

Implements Bourdoncle "Efficient chaotic iteration strategies with widenings" algorithm to compute a WTO.

val pretty_partition : Stdlib.Format.formatter -> node Wto.partition -> unit

val pretty_component : Stdlib.Format.formatter -> node Wto.component -> unit

val equal_component : node Wto.component -> node Wto.component -> bool

val equal_partition : node Wto.partition -> node Wto.partition -> bool