Uses of Class
eu.bandm.tools.lljava.absy.LLJava.StackFrame

Packages that use LLJava.StackFrame

Package	Description
eu.bandm.tools.lljava.absy	Abstract Syntax of LLJava, representing the byte code instructions, the objects which contain byte code, and the attributes specific to byte code classes.

Uses of LLJava.StackFrame in eu.bandm.tools.lljava.absy

Fields in eu.bandm.tools.lljava.absy declared as LLJava.StackFrame

Modifier and Type	Field and Description
protected LLJava.StackFrame	LLJava.StackFrameDelta.next Generated by umod; model author's documentation MISSING.
protected LLJava.StackFrame	LLJava.Instruction.post The static stack frame postcondition for this instruction.
protected LLJava.StackFrame	LLJava.Instruction.pre The static stack frame precondition for this instruction.

Methods in eu.bandm.tools.lljava.absy that return LLJava.StackFrame

Modifier and Type	Method and Description
LLJava.StackFrame	LLJava.StackFrame.doclone() Clones this object.
LLJava.StackFrame	LLJava.StackFrameDelta.get_next() Generated by umod; model author's documentation MISSING.
LLJava.StackFrame	LLJava.Instruction.get_post() The static stack frame postcondition for this instruction.
LLJava.StackFrame	LLJava.Instruction.get_pre() The static stack frame precondition for this instruction.
LLJava.StackFrame	LLJava.StackFrame.initFrom(Object o0) Copies values of all common fields from the argument.
LLJava.StackFrame	LLJava.StackFrame.with_locals(CheckedList<LLJava.VType> val) Generated by umod; model author's documentation MISSING.
LLJava.StackFrame	LLJava.StackFrame.with_operands(CheckedList<LLJava.VType> val) Generated by umod; model author's documentation MISSING.
LLJava.StackFrame	LLJava.StackFrame.with_uninitThis(boolean val) Generated by umod; model author's documentation MISSING.

Methods in eu.bandm.tools.lljava.absy that return types with arguments of type LLJava.StackFrame

Modifier and Type	Method and Description
static Pattern<LLJava.StackFrame>	LLJava.StackFrame.get_locals(Pattern<? super CheckedList<LLJava.VType>> p) Lifts a pattern which matches the field value to one which matches this whole object.
static Pattern<LLJava.StackFrame>	LLJava.StackFrame.get_operands(Pattern<? super CheckedList<LLJava.VType>> p) Lifts a pattern which matches the field value to one which matches this whole object.
static Pattern<LLJava.StackFrame>	LLJava.StackFrame.get_uninitThis(Pattern<? super Boolean> p) Lifts a pattern which matches the field value to one which matches this whole object.
static Pattern<? super LLJava.StackFrame>	LLJava.__Patterns.term_StackFrame(Pattern<Object> superpattern, Pattern<? super CheckedList<LLJava.VType>> p_locals, Pattern<? super CheckedList<LLJava.VType>> p_operands, Pattern<? super Boolean> p_uninitThis)

Methods in eu.bandm.tools.lljava.absy with parameters of type LLJava.StackFrame

Modifier and Type	Method and Description
protected void	LLJava.MATCH_ONLY_00.action(LLJava.StackFrame e0)
protected void	LLJava.MultiVisitor.action(LLJava.StackFrame e0)
protected void	LLJava.Visitor.action(LLJava.StackFrame e0)
protected void	LLJava.__Formatter.action(LLJava.StackFrame el)
protected void	LLJava.MultiVisitor.descend(LLJava.StackFrame e0)
void	LLJava.MATCH_ONLY_00.match(LLJava.StackFrame e0)
protected void	LLJava.MultiVisitor.post(LLJava.StackFrame e0)
protected void	LLJava.MultiVisitor.pre(LLJava.StackFrame e0)
boolean	LLJava.Instruction.set_post(LLJava.StackFrame val) The static stack frame postcondition for this instruction.
boolean	LLJava.Instruction.set_pre(LLJava.StackFrame val) The static stack frame precondition for this instruction.
protected Format	LLJava.__Formatter.toFormat(LLJava.StackFrame el)
LLJava.StackFrameDelta	LLJava.StackFrameDelta.with_next(LLJava.StackFrame val) Generated by umod; model author's documentation MISSING.
boolean	LLJava.StackFrame.x_equals(LLJava.StackFrame e0)

Method parameters in eu.bandm.tools.lljava.absy with type arguments of type LLJava.StackFrame

Modifier and Type	Method and Description
static Pattern<Object>	LLJava.__Patterns.cast_StackFrame(Pattern<? super LLJava.StackFrame> p)
static Pattern<LLJava.StackFrameDelta>	LLJava.StackFrameDelta.get_next(Pattern<? super LLJava.StackFrame> p) Lifts a pattern which matches the field value to one which matches this whole object.
static Pattern<LLJava.Instruction>	LLJava.Instruction.get_post(Pattern<? super LLJava.StackFrame> p) Lifts a pattern which matches the field value to one which matches this whole object.
static Pattern<LLJava.Instruction>	LLJava.Instruction.get_pre(Pattern<? super LLJava.StackFrame> p) Lifts a pattern which matches the field value to one which matches this whole object.
static Pattern<? super LLJava.Instruction>	LLJava.__Patterns.term_Instruction(Pattern<? super LLJava.Statement> superpattern, Pattern<? super LLJava.StackFrame> p_pre, Pattern<? super LLJava.StackFrame> p_post)
static Pattern<? super LLJava.Instruction>	LLJava.__Patterns.term_Instruction(Pattern<? super LLJava.Statement> superpattern, Pattern<? super LLJava.StackFrame> p_pre, Pattern<? super LLJava.StackFrame> p_post)
static Pattern<? super LLJava.StackFrameDelta>	LLJava.__Patterns.term_StackFrameDelta(Pattern<Object> superpattern, Pattern<? super Integer> p_delta, Pattern<? super LLJava.StackFrame> p_next)

Constructors in eu.bandm.tools.lljava.absy with parameters of type LLJava.StackFrame

Constructor and Description
StackFrameDelta(int delta, LLJava.StackFrame next) Constructor generated according to specification #0 Constructor defined according to directive "C 0/..".