entry_policy (library)

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.

    Documentation on imports

    This module has the following direct dependencies: