org.jmlspecs.checker
Class JMLWarningFilter

java.lang.Object
  org.multijava.mjc.DefaultFilter
      org.jmlspecs.checker.JMLWarningFilter

All Implemented Interfaces:

WarningFilter

Direct Known Subclasses:

JMLDefaultWarningFilter

public class JMLWarningFilter

extends DefaultFilter

A warning filter for JML.

Author:

Gary T. Leavens

Field Summary

 

Fields inherited from interface org.multijava.util.compiler.WarningFilter

FLT_ACCEPT, FLT_FORCE, FLT_REJECT

 

Constructor Summary

JMLWarningFilter()

 

Method Summary
int	filter(CWarning warning)           Filters a warning

 

Methods inherited from class java.lang.Object

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

 

Constructor Detail

JMLWarningFilter

public JMLWarningFilter()

filter

public int filter(CWarning warning)

Filters a warning

Specified by:

filter in interface WarningFilter

Overrides:

filter in class DefaultFilter

Parameters:

warning - a warning to be filtred

Returns:

FLT_REJECT, FLT_FORCE, FLT_ACCEPT