Intermodular entry policy

This module provides the entry policy algorithms for modular analysis. The entry policy is determined by the entry_policy preprocessing flag.

Usage and interface

Documentation on exports

Usage:check_curr_entry_id(Id)

Checks that Id was an entry of the last fixpoint analysis.

  • The following properties should hold at call time:
    (nonvar/1)Id is currently a term which is not a free variable.

Usage:curr_entry_id(Id)

Enumerates the Ids of the entries of the last fixpoint analysis.

    Usage:get_entry_info(AbsInt,Sg,Proj)

    Provides on backtracking entry abstract substitutions for the current module in the global level of intermodular analysis. In the case of manual scheduling, this predicate should be called for every module in the program unit. In the case of automatic scheduling, this predicate should only be called with top-level(U).

    • The following properties should hold at call time:
      (nonvar/1)AbsInt is currently a term which is not a free variable.
      (var/1)Sg is a free variable.
      (var/1)Proj is a free variable.

    Usage:

    User-specified entry points for intermodular analysis. I.e., according to the policy defined

      Usage:add_entries_to_registry(AbsInt)

      • The following properties should hold at call time:
        (nonvar/1)AbsInt is currently a term which is not a free variable.
        (atm/1)AbsInt is an atom.
      • The following properties should hold globally:
        (not_fails/1)All the calls of the form add_entries_to_registry(AbsInt) do not fail.