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 (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Wto/index.html

Module `Frama_c_kernel.Wto`

Weak topological orderings (WTOs) are a hierarchical decomposition of the a graph where each layer is topologically ordered and strongly connected components are aggregated and ordered recursively. This is a very convenient representation to describe an evaluation order to reach a fixpoint.

type 'n component =

| Component of 'n * 'n partition
(*
A strongly connected component, described by its head node and the remaining sub-components topologically ordered
*)
| Node of 'n
(*
A single node without self loop
*)

Each component of the graph is either an individual node of the graph (without) self loop, or a strongly connected component where a node is designed as the head of the component and the remaining nodes are given by a list of components topologically ordered.

and 'n partition = 'n component list

A list of strongly connected components, sorted topologically

val head : 'n partition -> 'n option

Return the first node of a partition or None if the partition is empty

val flatten : 'n partition -> 'n list

Transform the partition into a list

val fold_heads : ('a -> 'n -> 'a) -> 'a -> 'n partition -> 'a

module Make (Node : sig ... end) : sig ... end

This functor provides the partitioning algorithm constructing a WTO.