In the PROBLEM section you define the underlying framework for your analysis.
You have to specify:
| direction |
The direction of your analysis,
either forward or backward |
| carrier |
The underlying lattice of the analysis.
This must be a complete lattice which can be a built-in type of PAG/WWW
or a complex type defined in the
TYPE section. |
| init |
The initial value at each node.
This can be any FULA expression
but will usually be the neutral element of the combine function
(e.g. bot for lub or top for glb). |
| init_start |
The initial value of all nodes that have no incoming edges.
Typically this is the start of the analysis
(the begin node of the main program for forward analyses
or the end node of the main program for backward analyses).
This can be any FULA expression. |
| combine |
The combine function specifies how information
from multiple incoming edges is combined at the entry of a node.
It can be one of the FULA operators
lub (least upper bound) or glb (greatest lower bound),
or the name of a FULA function.
This function can be one of the predefined functions intersect or union
if your carrier is a power set
(in fact, these are only alternative names for glb and lub in this case),
or any other function defined in the
SUPPORT section
which has type cType * cType -> cType
where cType is the type specified as the carrier. |
| The following items are optional: |
| equal |
You may specify your own comparison function that checks
whether the exit-information at a node has changed.
You specify the name of a SUPPORT function which must have type
cType * cType -> bool where cType is the type specified as the carrier.
The first argument is the old data flow value of the node,
the second argument is the new value.
If you do not specify an equal function,
the default function standard_equal(a,b) = (a=b) will be used. |
| widening |
You may specify a widening function that applies widening
if the equal function returns false (i.e. the information at a node has changed).
You specify the name of a SUPPORT function which must have type
cType * cType -> cType where cType is the type specified as the carrier.
The first argument is the old data flow value of the node,
the second argument is the new value. If you do not specify a widening function,
the default function standard_widen(a,b) = b will be used
(this function just returns the new value). |
| narrowing |
You may specify a narrowing function just like a widening function.
If you do not specify a narrowing function,
the default function standard_narrow(a,b) = b will be used. |
