public abstract static class LLJava.Instruction extends LLJava.Statement
Modifier and Type | Field and Description |
---|---|
protected LLJava.StackFrame |
post
The static stack frame postcondition for this
instruction.
|
protected LLJava.StackFrame |
pre
The static stack frame precondition for this
instruction.
|
location
format
Constructor and Description |
---|
Instruction()
Synthetic minimal constructor provided by the umod compiler.
|
Modifier and Type | Method and Description |
---|---|
LLJava.Instruction |
doclone()
Clones this object.
|
Format |
format()
Delivers a format object for pretty-printing by inheritance from some ancestor class.
|
LLJava.StackFrame |
get_post()
The static stack frame postcondition for this
instruction.
|
static Pattern<LLJava.Instruction> |
get_post(Pattern<? super LLJava.StackFrame> p)
Lifts a pattern which matches the field value to one which matches this
whole object.
|
LLJava.StackFrame |
get_pre()
The static stack frame precondition for this
instruction.
|
static Pattern<LLJava.Instruction> |
get_pre(Pattern<? super LLJava.StackFrame> p)
Lifts a pattern which matches the field value to one which matches this
whole object.
|
LLJava.Instruction |
initFrom(Object o0)
Copies values of all common fields from the argument.
|
boolean |
set_post(LLJava.StackFrame val)
The static stack frame postcondition for this
instruction.
|
boolean |
set_pre(LLJava.StackFrame val)
The static stack frame precondition for this
instruction.
|
toString
get_location, get_location, set_location
protected LLJava.StackFrame pre
TypeChecker
. LLJava.StackFrame
(maybe null)protected LLJava.StackFrame post
TypeChecker
. LLJava.StackFrame
(maybe null)public Instruction()
public LLJava.Instruction doclone()
Cloneable
is known
to be implemented.doclone
in class LLJava.Statement
public Format format()
format
in interface Formattable
format
in class LLJava.Statement
public LLJava.Instruction initFrom(Object o0)
initFrom
in class LLJava.Statement
public LLJava.StackFrame get_pre()
TypeChecker
. LLJava.StackFrame
(maybe
null)public boolean set_pre(LLJava.StackFrame val)
TypeChecker
. val
- the new value of type LLJava.StackFrame
(maybe null)pre
public LLJava.StackFrame get_post()
TypeChecker
. LLJava.StackFrame
(maybe
null)public boolean set_post(LLJava.StackFrame val)
TypeChecker
. val
- the new value of type LLJava.StackFrame
(maybe null)post
public static Pattern<LLJava.Instruction> get_pre(Pattern<? super LLJava.StackFrame> p)
LLJava.__Patterns
.public static Pattern<LLJava.Instruction> get_post(Pattern<? super LLJava.StackFrame> p)
LLJava.__Patterns
.see also the complete user documentation .