Interface AbstractState<StateT extends AbstractState<StateT>>

Type Parameters:
StateT - recursive generic type of the abstract state.
All Known Subinterfaces:
JvmHeapAbstractState<StateT>, MapAbstractState<KeyT,AbstractSpaceT>
All Known Implementing Classes:
HashMapAbstractState, JvmAbstractState, JvmForgetfulHeapAbstractState, JvmFrameAbstractState, JvmMemoryLocationAbstractState, JvmShallowHeapAbstractState, JvmValueAbstractState, ListAbstractState, SetAbstractState, StackAbstractState, ValueAbstractState

public interface AbstractState<StateT extends AbstractState<StateT>>
An AbstractState contains information about the program state.

Abstract states are meant as part of a join-semilattice representing the domain of the analysis and implement operations over this set. In particular the states should be able to determine whether they are below another state in the partial order and to calculate the least upper bound on the semilattice when another state is provided (i.e., join operation).

  • Method Summary

    Modifier and Type
    Method
    Description
    Creates a copy of itself.
    boolean
     
    default Precision
    Returns the Precision used by the PrecisionAdjustment.
    int
     
    default boolean
    isLess(StateT abstractStateT)
    Strictly compares itself to the abstractState.
    boolean
    isLessOrEqual(StateT abstractState)
    Compares itself to the abstractState (i.e., compare the states on the partial order provided by the domain of the analysis).
    join(StateT abstractState)
    Computes a join over itself and another abstract state abstractState (i.e., finds the least upper bound on the semilattice).
  • Method Details

    • getPrecision

      default Precision getPrecision()
      Returns the Precision used by the PrecisionAdjustment.
    • copy

      StateT copy()
      Creates a copy of itself.
    • equals

      boolean equals(Object obj)
      Overrides:
      equals in class Object
    • hashCode

      int hashCode()
      Overrides:
      hashCode in class Object
    • join

      StateT join(StateT abstractState)
      Computes a join over itself and another abstract state abstractState (i.e., finds the least upper bound on the semilattice).
    • isLessOrEqual

      boolean isLessOrEqual(StateT abstractState)
      Compares itself to the abstractState (i.e., compare the states on the partial order provided by the domain of the analysis).
    • isLess

      default boolean isLess(StateT abstractStateT)
      Strictly compares itself to the abstractState.