Messages

method | MessageType[] values()
post | return_value == &new MessageType[](values#1)
post | new MessageType[](values#1) num objects == 1
post | return_value.length == 3
post | return_value[...] == ENUM$VALUES[...]

method | MessageType valueOf(String)
post | init'ed(return_value)

method | net.sourceforge.pebble.domain.MessageType__static_ init
post | ENUM$VALUES == &new MessageType[](MessageType__ static_init#4)
post | ERROR == &new MessageType(MessageType__static_ init#3)
post | ENUM$VALUES[2] == &new MessageType(MessageType_ _static_init#3)
post | INFO == &new MessageType(MessageType__static_ init#1)
post | ENUM$VALUES[0] == &new MessageType(MessageType_ _static_init#1)
post | WARN == &new MessageType(MessageType__static_ init#2)
post | ENUM$VALUES[1] == &new MessageType(MessageType_ _static_init#2)
post | new MessageType(MessageType__static_init#1) num objects == 1
post | new MessageType(MessageType__static_init#2) num objects == 1
post | new MessageType(MessageType__static_init#3) num objects == 1
post | new MessageType[](MessageType__static_init#4) num objects == 1
post | INFO.id == &"info"
post | INFO.name == &"Info"
post | WARN.id == &"warning"
post | WARN.name == &"Warning"
post | ERROR.id == &"error"
post | ERROR.name == &"Error"
post | ENUM$VALUES.length == 3
unanalyzed | call on java.lang.Enum

method | void net.sourceforge.pebble.domain. MessageType(String, int, String, String)
post | this.id == id
post | init'ed(this.id)
post | this.name == name
post | init'ed(this.name)

method | String getId()
pre | init'ed(this.id)
post | return_value == this.id
post | init'ed(return_value)

method | String getName()
pre | init'ed(this.name)
post | return_value == this.name
post | init'ed(return_value)