JmlAdmissibilityVisitor.NotAdmissibleException (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV CLASS NEXT CLASS

FRAMES NO FRAMES

SUMMARY: NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.checker
Class JmlAdmissibilityVisitor.NotAdmissibleException

java.lang.Object
  java.lang.Throwable
      java.lang.Exception
          java.lang.RuntimeException
              org.jmlspecs.checker.JmlAdmissibilityVisitor.NotAdmissibleException

All Implemented Interfaces:: Serializable

Enclosing class:: JmlAdmissibilityVisitor

protected class JmlAdmissibilityVisitor.NotAdmissibleException
extends RuntimeException

An Exception which is thrown when some was found not to be admissible. This Exception is a subclass of RuntimeException, since otherwise the signature of JExpression.accept(MjcVisitor) must be changed. Currently this exception is caught by checkAdmissibility.

Field Summary

Fields inherited from class java.lang.RuntimeException

Fields inherited from class java.lang.Throwable

Constructor Summary

protected JmlAdmissibilityVisitor.NotAdmissibleException()

Method Summary

Methods inherited from class java.lang.Throwable

fillInStackTrace, getCause, getLocalizedMessage, getMessage, getStackTrace, initCause, printStackTrace, printStackTrace, printStackTrace, setStackTrace, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

JmlAdmissibilityVisitor.NotAdmissibleException

protected JmlAdmissibilityVisitor.NotAdmissibleException()