plai_db (library)

Usage and interface

Documentation on exports

PREDICATEcomplete/7
complete(SgKey,AbsInt,Sg,Proj,Prime,Id,Parents)

The predicate SgKey has a variant success pattern (Sg,Proj,Prime) on the domain AbsInt. The and-or graph node is Id, and is called from the program points in list Parents. The predicate is of type data.

lub_complete(SgKey,AbsInt,Lub,Sg,Proj,Prime)

The predicate SgKey has in all variants success pattern (Sg,Proj,Prime) on the domain AbsInt. If Lub is yes, Proj and Prime are substitutions, if Lub is no, they are lists of substitutions. The predicate is of type data.

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

PREDICATEmemo_table/6
memo_table(PointKey,AbsInt,Id,Child,Vars_u,Call)

Before calling the goal at program point PointKey, there is a variant in which Call on the domain AbsInt holds upon the program clause variables Vars_u. These variables need be sorted conveniently so that Call makes sense. The and-or graph node that causes this is Id and the call originated to the goal at this program point generates and-or graph node Child. The predicate is of type data.

PREDICATEmemo_lub/5
memo_lub(PointKey,AbsInt,Lub,Vars_u,Call)

Before calling the goal at program point PointKey, in all variants Call on the domain AbsInt holds upon the program clause variables Vars_u. If Lub is yes, Call is a substitution, if If Lub is no, Call is a list of substitutions. The predicate is of type data.

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

complete_parent(Id,Parents)

Used to keep the trace of the parents in the and-or graph for the di fixpoint. The parents are used to choose previous aproximations to apply the widening operators on calls The and-or graph node is Id, and Parents is a list of couples of graph node and program points. The predicate is of type data.

cleanup_plai_db(AbsInt)

Erases all data in this module for the analysis domain AbsInt.

Usage:get_parent_key(LitKey,Id,AbsInt,CKey)

CKey is the key that corresponds to Id, it may not correspong to the decoding LitKey because of how meta_calls are indexed in the fixpoints

    Documentation on imports

    This module has the following direct dependencies: