Index of values

Compute the least upper bound of the current value of the vertex/variable with the values propagated by the incoming hyperedges belonging to the working set.

add tbl x y adds a binding of x to y in table tbl.

add x s returns a set containing all elements of s, plus x.

add x s returns a set containing all elements of s, plus x.

Add an hyperedge.

Add a vertex

Same as FixpointStd.analysis, but with the technique of Gopan and Reps published in Static Anlaysis Symposium, SAS'2007.

Main user function: analysis manager equation_graph sinit strategy takes a graph giving the structure of the equation system, a manager indicating how to interpret the equation system, a (super)set of the variables to be initialized to a non-empty value, and an iteration strategy.

Dynamic analysis.

Same as Fixpoint.analysis_std, but with the technique of Gopan and Reps published in Static Anlaysis Symposium, SAS'2007.

Performs initialization, fixpoint analysis and descending, and measures the global analysis time.

Append two lists

Print an array

Create a list element from a single element.

attrhedge graph hedge returns the information associated to the hyperedge hedge

attrvertex graph vertex returns the information associated to the vertex vertex

Return the number of elements of a set.

Return the number of elements of a set.

Decomposition of the graph into Strongly Connected Components,

idem, but from several initial vertices.

Return one element of the given set, or raise Not_found if the set is empty.

Return one element of the given set, or raise Not_found if the set is empty.

Remove all vertices and hyperedges of the graph.

Empty a hash table.

Total ordering between sets.

Total ordering between sets.

Adding a new list element at the begining of the list

Copy an hypergraph, using the given functions to duplicate the attributes associated to the elements of the graph.

Return a copy of the given hashtable.

create n data creates an hypergraph, using n for the initial size of internal hashtables, and data for the user information

create n creates a new, empty hash table, with initial size n.

Return the (maximal) depth of the list.

(Rather internal)

Internal functions

Set difference.

Union, intersection and set difference.

Prints internal graph on the (optional) formatter man.dot_fmt, see type FixpointType.manager.

Return the list of all elements of the given set.

Return the list of all elements of the given set.

The empty set.

The empty set.

The equality predicate used to compare keys.

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

Generate from a graph a function of type ('vertex, 'hedge) equation or dynamically exploring the graph.

Escape a string, replacing line breaks by linebreak (default '\n').

Existence test

exists p s checks if at least one element of the set satisfies the predicate p.

exists p s checks if at least one element of the set satisfies the predicate p.

filter p s returns the set of all elements in s that satisfy predicate p.

filter p s returns the set of all elements in s that satisfy predicate p.

find tbl x returns the current binding of x in tbl, or raises Not_found if no such binding exists.

find_all tbl x returns the list of all data associated with x in tbl.

Flatten the recursive list, only starting from the given

fold f tbl init computes (f kN dN ... (f k1 d1 init)...), where k1 ... kN are the keys of all bindings in tbl, and d1 ... dN are the associated values.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

Ordinary fold function for atoms, from left to right.

Ordinary fold function for atoms, from right to left.

for_all p s checks if all elements of the set satisfy the predicate p.

for_all p s checks if all elements of the set satisfy the predicate p.

Generate from an equation a graph, using make_attrvertex, make_attrhedge and info.

A hashing function on keys.

hash x associates a positive integer to any value of any type.

Print an hashtable

hash_param n m x computes a hash value for x, with the same properties as for hash.

Return the head of the list.

A dummy (never used) value for hyperedge identifiers (used for the functions XXX_multi)

Inference functions, taking a standard manager, a threshold manager, an equation graph, and an iteration strategy.

info g returns the user-information attached to the graph g

init manager input sinit creates the internal graph structure (from the equation graph input) and initialize the working sets (from the set of initial points sinit) (stored in the info field of the internal graph).

Set intersection.

Is the graph empty ?

Test whether a set is empty or not.

Test whether a set is empty or not.

Does the array of vertices belong to the graph, all with non bottom values ?

Ordinary iteration function for atoms

iter f tbl applies f to all bindings in table tbl.

iter f s applies f in turn to all elements of s.

iter f s applies f in turn to all elements of s.

Iterates the function f hedge attrhedge succvertices predvertices to all hyperedges of the graph.

Iterates the function f vertex attrvertex succhedges predhedges to all vertices of the graph.

Return the ength of the list.

length tbl returns the number of bindings in tbl.

Create a list element from a list.

Print a list

Build a "default" strategy, with the following options:

Build a "default" strategy, with the following options:

Ordinary map function

map f tbl applies f to all bindings in table tbl and creates a new hashtable associating the results of f to the same key type.

Return the set of vertices without successor hyperedges

Same as Sette.S.min_elt, but returns the largest element of the given set.

Same as min_elt, but returns the largest element of the given set.

Membership test.

mem tbl x checks if x is bound in tbl.

mem x s tests whether x belongs to the set s.

mem x s tests whether x belongs to the set s.

Return the set of vertices without predecessor hyperedges

Return the smallest element of the given set (with respect to the Ord.compare ordering), or raise Not_found if the set is empty.

Return the smallest element of the given set (with respect to the Ord.compare ordering), or raise Not_found if the set is empty.

Create a recursive list from a regular list

Print an optional element

(Rather internal function)

Print a pair

partition p s returns a pair of sets (s1, s2), where s1 is the set of all the elements of s that satisfy the predicate p, and s2 is the set of all the elements of s that do not satisfy p.

partition p s returns a pair of sets (s1, s2), where s1 is the set of all the elements of s that satisfy the predicate p, and s2 is the set of all the elements of s that do not satisfy p.

Predecessor vertices of a vertex by any hyperedge

Predecessor hyperedges of a vertex

Predecessor vertices of an hyperedge

Print a graph in textual format on the given formatter, using the given functions to resp.

Printing function.

Output the graph in DOT format on the given formatter, using the given functions to resp print:

Prints internal graph.

Transforms a conversion-to-string function to a printing function.

Prints the result of an analysis.

Prints the result of an analysis.

Prints statistics

Prints statistics

print_strategy_vertex man fmt sv prints an object of type strategy, using the manager man for printing vertices and hyperedges.

print_strategy_vertex man fmt sv prints an object of type strategy, using the manager man for printing vertices and hyperedges.

print_strategy_vertex man fmt sv prints an object of type strategy_vertex, using the manager man for printing vertices and hyperedges.

print_strategy_vertex man fmt sv prints an object of type strategy_vertex, using the manager man for printing vertices and hyperedges.

(Rather internal function)

Returns the set of vertices and hyperedges that are *NOT* reachable from the given root vertex.

remove tbl x removes the current binding of x in tbl, restoring the previous binding if it exists.

remove x s returns a set containing all elements of s, except x.

remove x s returns a set containing all elements of s, except x.

Remove the hyperedge from the graph.

Remove the vertex from the graph, as well as all related hyperedges.

replace tbl x y replaces the current binding of x in tbl by a binding of x to y.

Change the attribute of an existing hyperedge

Change the attribute of an existing vertex

Recursively reverse the recursive list rev [a;[b;[c];d];e;[f]] = [[f];e;[d;[c];b];a]

Decomposition of the graph into Strongly Connected Sub-Components,

idem, but from several initial vertices.

singleton x returns the one-element set containing only x.

singleton x returns the one-element set containing only x.

size graph returns (nbvertex,nbhedge,nbedgevh,nbedgehv)

Number of edges (hyperedge,vertex) in the hypergraph

Number of edges (vertex,hyperedge) in the hypergraph

Number of hyperedges in the hypergraph

Number of vertices in the hypergraph

Meant to be internal, but exporting needed for Mappe.maptoset.

Better sprintf function than Format.sprintf, as it takes the same kind of formatters as other Format.Xprintf functions.

Transforms a printing function into a conversion-to-string function.

subset s1 s2 tests whether the set s1 is a subset of the set s2.

subset s1 s2 tests whether the set s1 is a subset of the set s2.

Successor vertices of a vertex by any hyperedge

Successor hyperedges of a vertex

Successor vertices of an hyperedge

Return the tail of the list.

Create a regular list from a recursive list.

Topological sort of the vertices of the hypergraph starting from a root vertex.

Topological sort from a set of root vertices.

Similar to copy, but hyperedges are reversed: successor vertices and predecessor vertices are exchanged.

Return the array of abstract values associated to the vertices

Set union.

Update working sets assuming that the abstract value associated to the vertex has been modified.

A dummy (never used) value for vertex identifiers (used for the functions XXX_multi)

Print a weak pointer array

wrap_duration duration f executes the function f and stores into !duration the time spent in f, in seconds.

Similar to wrap_duration, but here the time spent in f is added to the value !duration.