module Make:
Parameters: |
|
module M:Map.S
with type key = G.V.t
Map used to store the result of the analysis
val recurse : ChaoticIteration.G.t ->
G.V.t WeakTopological.t ->
(G.V.t -> D.t) ->
G.V.t ChaoticIteration.widening_set -> int -> D.t M.t
recurse g wto init widening_set widening_delay
computes the
fixpoint of the analysis of a graph. This function uses the
recursive iteration strategy: it recursively stabilizes the
subcomponents of every component every time the component is
stabilized (cf. Bourdoncle's paper).
g
to their analysis result.g
: The graph to analyse.wto
: A weak topological ordering of the vertices of g
.init
: How to compute the initial analysis data.widening_set
: On which points to do the widening.widening_delay
: How many computations steps will be done
before using widening to speed up the stabilisation. This
counter is reset when entering each component, and is shared
between all outermost vertices of this component. A negative
value means 0
.