Package apron

Class Manager

java.lang.Object
apron.Manager
Direct Known Subclasses:
Box, Octagon, Polka, PolkaEq, PolkaGrid, PplGrid, Pplite, PplPoly
public class Manager extends Object
Class of numerical abstract domain instances.

Each abstract domain subclasses the Manager class to provide a Manager factory for the domain. The Manager is itself a factory for abstract elements in the corresponding abstract domain: abstract elements can be constructed and manipulated by passing the Manager instance to the Abstract0 and Abstract1 classes.

A Manager stores a set of abstract domain configuration parameters to tune the cost/precision of the instance of the abstract domain.

Finally, a Manager stores thread-local information. It is safe to call all Apron methods in concurrent threads as long as all arguments (including this, and including the Manager argument) are distinct in all threads.

A Manager object encapsulates an ap_manager_t Apron object allocated in the C heap.

  • Field Details

  • Constructor Details

    • Manager

      protected Manager()
      Managers can only be constructed from an abstract domain Manager subclass.

  • Method Details

    • finalize

      protected void finalize()
      Deallocates the Apron ap_manager_t object.
      Overrides:
      finalize in class Object

    • getLibrary

      public String getLibrary()
      Returns the name of the numerical abstract domain library that created the manager.

    • getVersion

      public String getVersion()
      Returns the version of the numerical abstract domain library that created the manager.

    • getAlgorithm

      public int getAlgorithm(int funid)
      Returns the current precision level chosen for the given operation (FUNID_COPY, etc.).

    • getTimeout

      public int getTimeout(int funid)
      Returns the current timeout value chosen for the given operation (FUNID_COPY, etc.).

    • getMaxObjectSize

      public int getMaxObjectSize(int funid)
      Returns the memory size limit chosen for the given operation (FUNID_COPY, etc.).

    • getFlagExactWanted

      public boolean getFlagExactWanted(int funid)
      Whether the given operation updates the exactness flag (FUNID_COPY, etc.)..

    • getFlagBestWanted

      public boolean getFlagBestWanted(int funid)
      Whether the given operation updates the best-precision flag (FUNID_COPY, etc.).

    • setAlgorithm

      public void setAlgorithm(int funid, int precision)
      Sets the current precision level for the given operation. (FUNID_COPY, etc.).

      0 is the default. Negative numbers indicate less precision, while positive numbers indicate more precision.

      The exact meaning of each value depends on the abstract domain.

    • setTimeout

      public void setTimeout(int funid, int time)
      Sets a timeout for the given operation (FUNID_COPY, etc.).

      Note: timeouts are currently unimplemented.

    • setMaxObjectSize

      public void setMaxObjectSize(int funid, int size)
      Sets a size limit on the memory used by the given operation (FUNID_COPY, etc.).

      By default, there is no limit.

      The unit is domain-specific but is consistent with the result of Abstract0.getSize(apron.Manager).

      0 indicates no limit.

    • setFlagExactWanted

      public void setFlagExactWanted(int funid, boolean wanted)
      Whether the given operation (FUNID_COPY, etc.) should update the exactness flag.

      As computing the exactness information may be costly, it is disabled by default for all operations.

    • setFlagBestWanted

      public void setFlagBestWanted(int funid, boolean wanted)
      Whether the given operation (FUNID_COPY, etc.) should update the best-precision flag.

      As computing the best-precision information may be costly, it is disabled by default for all operations.

    • wasExact

      public boolean wasExact()
      Whether the last operation with setFlagExactWanted(int, boolean) set returned an exact result.

    • wasBest

      public boolean wasBest()
      Whether the last operation with setFlagBestWanted(int, boolean) set returned a result which is optimal with respect to the abstraction.

    • getPreferedScalarType

      public int getPreferedScalarType()
      Gets the currently chosen preferred scalar type (SCALAR_DOUBLE, etc.).

    • setPreferedScalarType

      public void setPreferedScalarType(int t)
      Sets a preferred scalar type (SCALAR_DOUBLE, etc.).