fixpo_dd (library)

Stability: [devel] Currently the subject of active development and/or research. Functionality may be limited and API and/or functionality may change without warning or deprecation period. Not recommended yet for use in production.


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.

Usage:add_external_complete_change(AbsInt,NewPrime,SgKey,Sg,Id,Proj)

This predicate updates analysis information given a complete that has changed externally. Typically this is used for updating completes that are outdated as a consequence of modular analysis (the analysis of a module was improved). The complete that has change has key SgKey and id Id. The new answer for the complete is NewPrime and refers to domain AbsInt.

Changes in answers are updated as follows:

  • If the new answer is more general than the previous one, the update is as simple as replacing the answer in the complete and adding an event.

  • If the new answer is more specific or incompatible, the information that depends on it has to be deleted and recomputed. We are removing the information with a top-down deletion strategy, although a bottom-up deletion strategy could more efficient. The fixpoint has to be runned after this deletion.

  • The following properties should hold at call time:
    (atm/1)AbsInt is an atom.
    (list/1)NewPrime is a list.
    (atm/1)SgKey is an atom.
    (atm/1)Id is an atom.