daikon.tools.jtb
Class Annotate

Object
  Annotate

public class Annotate
extends Object

Merge Daikon-generated invariants into Java source code as ESC/JML/DBC annotations. All original .java files are left unmodified; copies are created.

The first argument is a Daikon .inv file -- a serialized file of Invariant objects. All subsequent arguments are Foo.java files that are rewritten into Foo.java-jmlannotated versions; alternately, use the -r flag to process every .java file under the current directory.

Field Summary

static Logger	debug
static String	max_invariants_pp_SWITCH
static String	no_reflection_SWITCH
static String	wrapXML_SWITCH

Constructor Summary

Annotate()

Method Summary

static void	main(String[] args)
static void	mainHelper(String[] args) This does the work of main, but it never calls System.exit, so it is appropriate to be called progrmmatically.

Methods inherited from class Object

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

Field Detail

debug

public static final Logger debug

wrapXML_SWITCH

public static final String wrapXML_SWITCH

See Also:

Constant Field Values

max_invariants_pp_SWITCH

public static final String max_invariants_pp_SWITCH

See Also:

Constant Field Values

no_reflection_SWITCH

public static final String no_reflection_SWITCH

See Also:

Constant Field Values

Constructor Detail

Annotate

public Annotate()

Method Detail

main

public static void main(String[] args)
                 throws Exception

Throws:

Exception

mainHelper

public static void mainHelper(String[] args)
                       throws Exception

This does the work of main, but it never calls System.exit, so it is appropriate to be called progrmmatically. Termination of the program with a message to the user is indicated by throwing Daikon.TerminationMessage.

Throws:

Exception

See Also:

main(String[]), Daikon.TerminationMessage