Class JvmDefaultExpandOperator<StateT extends LatticeAbstractState<StateT>>

    • Constructor Detail

      • JvmDefaultExpandOperator

        public JvmDefaultExpandOperator​(JvmCfa cfa)
        Create the default expand operator for the JVM.
        Parameters:
        cfa - the control flow automaton of the analyzed program
      • JvmDefaultExpandOperator

        public JvmDefaultExpandOperator​(JvmCfa cfa,
                                        boolean expandHeap)
        Create the default expand operator for the JVM.
        Parameters:
        cfa - the control flow automaton of the analyzed program
        expandHeap - whether expansion of the heap is performed
    • Method Detail

      • expand

        public JvmAbstractState<StateT> expand​(AbstractState expandedInitialState,
                                               AbstractState reducedExitState,
                                               JvmCfaNode blockEntryNode,
                                               Call call)
        Description copied from interface: ExpandOperator
        Reconstructs the state of the caller of a procedure using the information of the expanded initial state, the reduced exit state, the block entry node (that can be used to retrieve the CFA subgraph of the function), and the call to the procedure.
        Specified by:
        expand in interface ExpandOperator<JvmCfaNode,​JvmCfaEdge,​MethodSignature>
        Parameters:
        expandedInitialState - the entry state of the called procedure before any reduction
        reducedExitState - the state of the called procedure in its exit node
        blockEntryNode - the entry node of the called procedure
        call - the information of the call to the procedure
        Returns:
        The state of the caller after the procedure call, eventually with some collisions of identifiers that need the RebuildOperator to be solved
      • calculateReturnValues

        protected java.util.List<StateT> calculateReturnValues​(AbstractState reducedExitState,
                                                               Instruction returnInstruction,
                                                               Call call)
        Calculates the returned state. Can be overridden to handle special behavior.