Package org.mpi_sws.jmc.annotations

package org.mpi_sws.jmc.annotations
Defines annotations used by users of the JMC library.
  • Annotation Interfaces
    Class
    Description
    JmcCheck
    A mandatory annotation to mark a test method or class to be run with the JMC model checker.
    JmcCheckConfiguration
    Configuration annotation for JMC checks.
    JmcExpectAssertionFailure
    This annotation is used to mark a test method or class to expect an assertion failure in the JMC model checker.
    JmcExpectExecutions
    This annotation is used to mark a test method or class to expect a certain number of executions in the JMC model checker.
    JmcIgnoreInstrumentation
    This annotation is used to mark methods or classes that should be ignored by the JMC instrumentation.
    JmcReplay
    This annotation is used to mark a test method or class to be replayed in the JMC model checker.
    JmcTimeout
    This annotation is used to specify a timeout for a test method or class when using the JMC model checker.