dk.brics.tajs.monitoring

Class TAJSAssertionReachabilityCheckerMonitor

java.lang.Object

dk.brics.tajs.monitoring.DefaultAnalysisMonitoring

dk.brics.tajs.monitoring.TAJSAssertionReachabilityCheckerMonitor

All Implemented Interfaces:

ILatticeMonitoring, IAnalysisMonitoring, ISolverMonitoring<State,Context>

public class TAJSAssertionReachabilityCheckerMonitor
extends DefaultAnalysisMonitoring

Monitor for checking TAJS_*-assertions are reachable at the end of the scan phase..

To be used for testing: asserts that syntactic TAJS_assert and TAJS_assertEqual calls are invoked.

Rationale: TAJS_asserts that are unreachable are probably unintended!

Special case: TAJS_assert(false) is not supposed to be reachable.

Constructor Summary

Constructors

Constructor and Description
TAJSAssertionReachabilityCheckerMonitor(java.util.function.Supplier<java.lang.Boolean> analysisReachedFixedPoint)

Method Summary

Modifier and Type	Method and Description
void	setSolverInterface(GenericSolver.SolverInterface c) Sets the solver interface which will be used by the analysis.
void	visitNodeTransferPre(AbstractNode n, State s) Invoked immediately before processing a node transfer.
void	visitPhasePost(AnalysisPhase phase) Invoked at the end of a phase.
void	visitPhasePre(AnalysisPhase phase) Invoked at the beginning of a phase.

Methods inherited from class dk.brics.tajs.monitoring.DefaultAnalysisMonitoring

addMessage, addMessage, addMessageInfo, allowNextIteration, getMessages, getTypeInformation, visitBlockTransferPost, visitBlockTransferPre, visitCall, visitEvalCall, visitEventHandlerRegistration, visitFunction, visitIf, visitIn, visitInnerHTMLWrite, visitInstanceof, visitIterationDone, visitJoin, visitNativeFunctionCall, visitNativeFunctionReturn, visitNewFlow, visitNewObject, visitNodeTransferPost, visitPropagationPost, visitPropagationPre, visitPropertyAccess, visitPropertyRead, visitPropertyWrite, visitRead, visitReadNonThisVariable, visitReadProperty, visitReadThis, visitReadVariable, visitRecoveryGraph, visitRenameObject, visitUnknownValueResolve, visitUserFunctionCall, visitVariableAsRead, visitVariableOrProperty

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

TAJSAssertionReachabilityCheckerMonitor

public TAJSAssertionReachabilityCheckerMonitor(java.util.function.Supplier<java.lang.Boolean> analysisReachedFixedPoint)

Method Detail

setSolverInterface

public void setSolverInterface(GenericSolver.SolverInterface c)

Description copied from interface: IAnalysisMonitoring

Sets the solver interface which will be used by the analysis.

Specified by:

setSolverInterface in interface IAnalysisMonitoring

Overrides:

setSolverInterface in class DefaultAnalysisMonitoring

visitNodeTransferPre

public void visitNodeTransferPre(AbstractNode n,
                                 State s)

Description copied from interface: ISolverMonitoring

Invoked immediately before processing a node transfer.

Specified by:

visitNodeTransferPre in interface ISolverMonitoring<State,Context>

Overrides:

visitNodeTransferPre in class DefaultAnalysisMonitoring

visitPhasePost

public void visitPhasePost(AnalysisPhase phase)

Description copied from interface: IAnalysisMonitoring

Invoked at the end of a phase.

Specified by:

visitPhasePost in interface IAnalysisMonitoring

Overrides:

visitPhasePost in class DefaultAnalysisMonitoring

visitPhasePre

public void visitPhasePre(AnalysisPhase phase)

Description copied from interface: IAnalysisMonitoring

Invoked at the beginning of a phase.

Specified by:

visitPhasePre in interface IAnalysisMonitoring

Overrides:

visitPhasePre in class DefaultAnalysisMonitoring