jml2b.pog.util
Class ColoredInfo

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.util.ColoredInfo

All Implemented Interfaces:

java.io.Serializable

public class ColoredInfo

extends Profiler

implements java.io.Serializable

This class defines informations associated to formula in order to color the code in the viewer.

Author:

L. Burdy

See Also:

Serialized Form

Field Summary

static byte	EQUALS_0 comment indice corresponding to a ArithmeticException (red).
static byte	IS_FALSE comment indice corresponding to a test considered as false (blue).
static byte	IS_NEGATIVE comment indice corresponding to a NegativeArraySizeException (red).
static byte	IS_NOT_CASTABLE comment indice corresponding to a ClassCastException (red).
static byte	IS_NOT_STORABLE comment indice corresponding to a ArrayStoreException (red)
static byte	IS_NULL comment indice corresponding to a NullPointerException (red).
static byte	IS_OUT_OF_BOUNDS comment indice corresponding to a ArrayIndexOutOfBoundException (red)
static byte	IS_TRUE comment indice corresponding to a test considered as true (blue).
static byte	METHOD_CALL comment indice corresponding to the call of a method (blue).
static byte	NEW comment indice corresponding to an object creation (blue).
static byte	THROWS_EXCEPTION comment indice corresponding to an exception thrown by a method call (red)

Constructor Summary

ColoredInfo()
Constructs a colored info with no coloration.

ColoredInfo(ParsedItem b)
Constructs a green colored info

ColoredInfo(ParsedItem b, byte c)
Constructs a red colored info or a blue without additional informations.

ColoredInfo(ParsedItem b, byte c, java.lang.String s)
Constructs a blue colored info with informations.

Method Summary

byte	getComment()
int	getIndex()
void	save(JpoOutputStream s, int index, JmlFile f) Saves the colored info in a .jpo file if it is declared in a specified JML file

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Field Detail

IS_TRUE

public static final byte IS_TRUE

comment indice corresponding to a test considered as true (blue).

See Also:

Constant Field Values

IS_FALSE

public static final byte IS_FALSE

comment indice corresponding to a test considered as false (blue).

See Also:

Constant Field Values

IS_NOT_CASTABLE

public static final byte IS_NOT_CASTABLE

comment indice corresponding to a ClassCastException (red).

See Also:

Constant Field Values

IS_NEGATIVE

public static final byte IS_NEGATIVE

comment indice corresponding to a NegativeArraySizeException (red).

See Also:

Constant Field Values

IS_NULL

public static final byte IS_NULL

comment indice corresponding to a NullPointerException (red).

See Also:

Constant Field Values

EQUALS_0

public static final byte EQUALS_0

comment indice corresponding to a ArithmeticException (red).

See Also:

Constant Field Values

IS_NOT_STORABLE

public static final byte IS_NOT_STORABLE

comment indice corresponding to a ArrayStoreException (red)

See Also:

Constant Field Values

IS_OUT_OF_BOUNDS

public static final byte IS_OUT_OF_BOUNDS

comment indice corresponding to a ArrayIndexOutOfBoundException (red)

See Also:

Constant Field Values

THROWS_EXCEPTION

public static final byte THROWS_EXCEPTION

comment indice corresponding to an exception thrown by a method call (red)

See Also:

Constant Field Values

METHOD_CALL

public static final byte METHOD_CALL

comment indice corresponding to the call of a method (blue).

See Also:

Constant Field Values

NEW

public static final byte NEW

comment indice corresponding to an object creation (blue).

See Also:

Constant Field Values

Constructor Detail

ColoredInfo

public ColoredInfo()

Constructs a colored info with no coloration.

ColoredInfo

public ColoredInfo(ParsedItem b)

Constructs a green colored info

ColoredInfo

public ColoredInfo(ParsedItem b,
                   byte c)

Constructs a red colored info or a blue without additional informations.

ColoredInfo

public ColoredInfo(ParsedItem b,
                   byte c,
                   java.lang.String s)

Constructs a blue colored info with informations.

Method Detail

save

public void save(JpoOutputStream s,
                 int index,
                 JmlFile f)
          throws java.io.IOException

Saves the colored info in a .jpo file if it is declared in a specified JML file

Parameters:

s - output stream for the jpo files

Throws:

java.io.IOException

See Also:

VirtualFormula#save(DataOutputStream, int, JmlFile), Theorem#save(DataOutputStream, JmlFile)

getIndex

public int getIndex()

getComment

public byte getComment()

Returns: