jack.plugin.source
Class RequiresGenerator

java.lang.Object
  jack.plugin.RunnableWithError
      jack.plugin.source.JmlClauseGenerator
          jack.plugin.source.RequiresGenerator

All Implemented Interfaces:

org.eclipse.jface.operation.IRunnableWithProgress

public class RequiresGenerator

extends JmlClauseGenerator

Generator of requires clause.

Author:

L. Burdy

Constructor Summary

RequiresGenerator(IJml2bConfiguration config, org.eclipse.swt.widgets.Shell shell, JmlFile jf, boolean reqNullPointer, boolean reqArryOutOfBounds)

Methods inherited from class jack.plugin.source.JmlClauseGenerator

getUpdated, run, setMethods

Methods inherited from class jack.plugin.RunnableWithError

getErrorDescription, getErrorDetails, hasDetails, hasSucceeded

Methods inherited from class java.lang.Object

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

Constructor Detail

RequiresGenerator

public RequiresGenerator(IJml2bConfiguration config,
                         org.eclipse.swt.widgets.Shell shell,
                         JmlFile jf,
                         boolean reqNullPointer,
                         boolean reqArryOutOfBounds)