transfer

This method is executed for each EOG edge which is in the worklist. currentEdge is the edge to process, currentState contains the state which was observed before arriving here.

This method modifies the state for the next eog edge as follows:

• If the next node in the eog is an IfStatement, the condition is evaluated and if it is either always true or false, the else or then branch receives set to Reachability.UNREACHABLE.

• If the next node in the eog is a WhileStatement, the condition is evaluated and if it's always true or false, either the EOG edge to the loop body or out of the loop body is set to Reachability.UNREACHABLE.

• For all other nodes, we simply propagate the state which led us here.

Returns the updated state and true because we always expect an update of the state.