gov.nasa.jpf.vm

Class NoJPFExec

java.lang.Object

gov.nasa.jpf.vm.NoJPFExec

All Implemented Interfaces:

SystemAttribute

public class NoJPFExec
extends java.lang.Object
implements SystemAttribute

InfoObject attr that flags a certain construct (field, method, class) is not supposed to be used under JPF. Useful for model classes that have or use features which have to be cut off / abstracted by means of native peers, and we want to catch violations as early as possible

Field Summary

Fields

Modifier and Type	Field and Description
static NoJPFExec	SINGLETON

Constructor Summary

Constructors

Constructor and Description
NoJPFExec()

Method Summary

Methods inherited from class java.lang.Object

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

Field Detail

SINGLETON

public static final NoJPFExec SINGLETON

Constructor Detail

NoJPFExec

public NoJPFExec()