Package org.mpi_sws.jmc.annotations

Annotation Interface JmcCheck

@Target({METHOD,TYPE})
@Retention(RUNTIME)
@Testable
public @interface JmcCheck

A mandatory annotation to mark a test method or class to be run with the JMC model checker.