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

Library usage:
:- use_module(ciaopp(plai/fixpo_plai)).
Exports:
- Predicates:
  query/8, init_fixpoint/0, cleanup_fixpoint/1, entry_to_exit/9, approx/6, fixpoint/6.

Documentation on exports

PREDICATEquery/8

Usage: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.

The following properties should hold at call time:
(nonvar/1)AbsInt is currently a term which is not a free variable.
(nonvar/1)QKey is currently a term which is not a free variable.
(nonvar/1)Query is currently a term which is not a free variable.
(nonvar/1)Qv is currently a term which is not a free variable.
(nonvar/1)RFlag is currently a term which is not a free variable.
(nonvar/1)Call is currently a term which is not a free variable.
(var/1)Succ is a free variable.

PREDICATEinit_fixpoint/0

Usage:

Cleanups the database of analysis of temporary information.

PREDICATEcleanup_fixpoint/1

Usage:cleanup_fixpoint(AbsInt)

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

PREDICATEentry_to_exit/9

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.

Documentation on imports

This module has the following direct dependencies:

Application modules:
preprocess_flags, fixpo_ops, domains, plai_db, psets, transform, apply_assertions_old.
System library modules:
native_props, datafacts_rt, aggregates, lists, terms_vars, sets, sort, messages.
Internal (engine) modules:
term_basic, arithmetic, atomic_basic, basiccontrol, exceptions, term_compare, term_typing, debugger_support, basic_props, hiord_rt.
Packages:
prelude, initial, condcomp, assertions, assertions/assertions_basic, basicmodes, nativeprops, datafacts, ciaopp(ciaopp_options), .(notrace), spec(no_debug).