Class BlockAbstraction


  • public class BlockAbstraction
    extends java.lang.Object
    A block abstraction is a summary of the analysis of a procedure call, represented by the set of reached abstract states and a waitlist of states that still need to be analyzed. The BAM CPA can save these abstractions in a cache and retrieve them when the same procedure is called with the same entry AbstractState.
    • Constructor Detail

      • BlockAbstraction

        public BlockAbstraction​(ReachedSet reachedSet,
                                Waitlist waitlist)
        Create a new block abstraction.
        Parameters:
        reachedSet - a collection of discovered states
        waitlist - a collection of states of the block that need to be analyzed
    • Method Detail

      • getReachedSet

        public ReachedSet getReachedSet()
        Returns the ReachedSet of the block abstraction.
      • getWaitlist

        public Waitlist getWaitlist()
        Returns the Waitlist of the block abstraction.