fixpo_plai (library)

Author(s): Kalyan Muthukumar, Maria Garcia de la Banda, Francisco Bueno.

Stability: [alpha] A good part of the functionality is there but has not been the subject of significant testing and/or verification.


This module implements the top-down fixpoint algorithm of PLAI, both in its mono-variant and multi-variant on successes versions. It is always multi-variant on calls. The algorithm is parametric on the particular analysis domain.

Usage and interface

Documentation on exports

PREDICATEquery/8
query(AbsInt,QKey,Query,Qv,RFlag,N,Call,Succ)

The success pattern of Query with Call is Succ in the analysis domain AbsInt. The predicate called is identified by QKey, and RFlag says if it is recursive or not. The goal Query has variables Qv, and the call pattern is uniquely identified by N.

Cleanups the database of analysis of temporary information.

cleanup_fixpoint(AbsInt)

Cleanups the database of analysis, of both temporary as well as permanent information regarding abstract domain AbsInt.

No further documentation available for this predicate.

PREDICATEapprox/6
No further documentation available for this predicate. The predicate is of type data.

PREDICATEfixpoint/6
No further documentation available for this predicate. The predicate is of type data.

No further documentation available for this predicate. The predicate is of type data.

Documentation on imports

This module has the following direct dependencies: