public abstract class ProgramSVSort extends AbstractSort
Modifier and Type | Class and Description |
---|---|
private static class |
ProgramSVSort.ArrayInitializerSVSort
This sort represents a type of program schema variables that
match only on Array Initializers.
|
private static class |
ProgramSVSort.ArrayLengthSort |
private static class |
ProgramSVSort.ArrayPostDeclarationSort |
private static class |
ProgramSVSort.CatchSort
This sort represents a type of program schema variables that
match only on catch branches of try-catch-finally blocks
|
private static class |
ProgramSVSort.ConstantProgramVariableSort |
private static class |
ProgramSVSort.ExecutionContextSort |
private static class |
ProgramSVSort.ExpressionSort
This sort represents a type of program schema variables that match on
all expressions only.
|
private static class |
ProgramSVSort.ExpressionSpecialPrimitiveTypeSort
This sort represents a type of program schema variables that match
on simple expressions which have a special primitive type.
|
private static class |
ProgramSVSort.ForLoopSort |
private static class |
ProgramSVSort.ForUpdatesSort |
private static class |
ProgramSVSort.GuardSort |
private static class |
ProgramSVSort.LabelSort
This sort represents a type of program schema variables that match
on labels.
|
private static class |
ProgramSVSort.LeftHandSideSort
This sort represents a type of program schema variables that match
only on program variables or static field references with
a prefix that consists of a program variable followed by a
sequence of attribute accesses or of a type reference followed by
a sequence of attribute accesses
|
private static class |
ProgramSVSort.LocalVariableSort |
private static class |
ProgramSVSort.LoopInitSort |
private static class |
ProgramSVSort.MetaClassReferenceSort
This sort represents a type of program schema variables that
match only on meta class references.
|
private static class |
ProgramSVSort.MethodBodySort
This sort represents a type of program schema variables that
match only on method body statements
|
private static class |
ProgramSVSort.MethodNameSort
This sort represents a type of program schema variables that match
on names of method references, i.e. the "m" of o.m(p1,pn).
|
private static class |
ProgramSVSort.MultipleVariableDeclarationSort |
private static class |
ProgramSVSort.NewArraySVSort
This sort represents a type of program schema variables that match
only on Array Creation Expressions, new A[]
|
private static class |
ProgramSVSort.NonModelMethodBodySort
This sort represents a type of program schema variables that
match only on method body statements for nonmodel methods for which
an implementation is present.
|
private static class |
ProgramSVSort.NonSimpleExpressionNoClassReferenceSort |
private static class |
ProgramSVSort.NonSimpleExpressionSort
This sort represents a type of program schema variables that match
only on all expressions which are not matched by simple expression
SVs.
|
private static class |
ProgramSVSort.NonSimpleMethodReferenceSort
This sort represents a type of program schema variables that
match on a method call with SIMPLE PREFIX and AT LEAST a
NONSIMPLE expression in the ARGUMENTS.
|
private static class |
ProgramSVSort.NonSimpleNewSVSort
This sort represents a type of program schema variables that match
only on Class Instance Creation Expressions, new C(), where at
least one argument is a non-simple expression
|
private static class |
ProgramSVSort.NonStringLiteralSort
This sort represents a type of program schema variables that match
only on non-string literals
|
private static class |
ProgramSVSort.ProgramMethodSort
This sort represents a type of program schema variables that
match only on program methods
|
private static class |
ProgramSVSort.ProgramVariableSort
This sort represents a type of program schema variables that match
only on program variables or static field references with
a prefix that consists of a program variable followed by a
sequence of attribute accesses or of a type reference followed by
a sequence of attribute accesses.
|
static class |
ProgramSVSort.SimpleExpressionNonStringObjectSort |
private static class |
ProgramSVSort.SimpleExpressionSort
This sort represents a type of program schema variables that match
only on program variables or static field references with
a prefix that consists of a program variable followed by a
sequence of attribute accesses or of a type reference followed by
a sequence of attribute accesses (negated) literal
expressions or instanceof expressions v instanceof T with an
expression v that matches on a program variable SV
|
private static class |
ProgramSVSort.SimpleExpressionSpecialPrimitiveTypeSort
This sort represents a type of program schema variables that match
on simple expressions which have a special primitive type.
|
static class |
ProgramSVSort.SimpleExpressionStringSort
This sort represents a type of program schema variables that match
on string literals and string variables.
|
private static class |
ProgramSVSort.SimpleNewSVSort
This sort represents a type of program schema variables that match
only on Class Instance Creation Expressions, new C(), where all
arguments are simple expressions.
|
private static class |
ProgramSVSort.SpecialConstructorReferenceSort
This sort represents a type of program schema variables that
match only on Special Constructor References.
|
private static class |
ProgramSVSort.StatementSort
This sort represents a type of program schema variables that
match only on statements
|
private static class |
ProgramSVSort.StaticVariableSort |
private static class |
ProgramSVSort.StringLiteralSort
This sort represents a type of program schema variables that match
only string literals, e.g.
|
private static class |
ProgramSVSort.SwitchSVSort |
private static class |
ProgramSVSort.TypeReferenceNotPrimitiveSort
This sort represents a type of program schema variables that
match anything except byte, char, short, int, and long.
|
private static class |
ProgramSVSort.TypeReferenceSort
This sort represents a type of program schema variables that
match only on type references.
|
ANY, CAST_NAME, EXACT_INSTANCE_NAME, FORMULA, INSTANCE_NAME, TERMLABEL, UPDATE
Constructor and Description |
---|
ProgramSVSort(Name name) |
Modifier and Type | Method and Description |
---|---|
boolean |
canStandFor(ProgramElement check,
ExecutionContext ec,
Services services) |
protected abstract boolean |
canStandFor(ProgramElement check,
Services services) |
boolean |
canStandFor(Term t) |
ProgramSVSort |
createInstance(java.lang.String parameter) |
(package private) static KeYJavaType |
getKeYJavaType(ProgramElement pe,
ExecutionContext ec,
Services services) |
ProgramElement |
getSVWithSort(ExtList l,
java.lang.Class<?> alternative) |
(package private) static boolean |
implicit(ProgramElement pe) |
(package private) static boolean |
methodConstrReference(ProgramElement pe) |
static java.util.Map<Name,ProgramSVSort> |
name2sort() |
declarationString, extendsSorts, extendsSorts, extendsTrans, getCastSymbol, getExactInstanceofSymbol, getInstanceofSymbol, isAbstract, name, toString
private static final java.util.Map<Name,ProgramSVSort> name2sort
public static final ProgramSVSort LEFTHANDSIDE
public static final ProgramSVSort VARIABLE
public static final ProgramSVSort STATICVARIABLE
public static final ProgramSVSort LOCALVARIABLE
public static final ProgramSVSort SIMPLEEXPRESSION
public static final ProgramSVSort NONSIMPLEEXPRESSION
public static final ProgramSVSort NONSIMPLEEXPRESSIONNOCLASSREFERENCE
public static final ProgramSVSort EXPRESSION
public static final ProgramSVSort SIMPLE_NEW
public static final ProgramSVSort NONSIMPLE_NEW
public static final ProgramSVSort NEWARRAY
public static final ProgramSVSort ARRAYINITIALIZER
public static final ProgramSVSort SPECIALCONSTRUCTORREFERENCE
public static final ProgramSVSort.NonSimpleMethodReferenceSort NONSIMPLEMETHODREFERENCE
public static final ProgramSVSort STATEMENT
public static final ProgramSVSort CATCH
public static final ProgramSVSort METHODBODY
public static final ProgramSVSort NONMODELMETHODBODY
public static final ProgramSVSort PROGRAMMETHOD
public static final ProgramSVSort TYPE
public static final ProgramSVSort TYPENOTPRIMITIVE
public static final ProgramSVSort CLASSREFERENCE
public static final ProgramSVSort METHODNAME
public static final ProgramSVSort LABEL
public static final ProgramSVSort JAVABOOLEANEXPRESSION
public static final ProgramSVSort SIMPLEJAVABYTEEXPRESSION
public static final ProgramSVSort SIMPLEJAVACHAREXPRESSION
public static final ProgramSVSort SIMPLEJAVASHORTEXPRESSION
public static final ProgramSVSort SIMPLEJAVAINTEXPRESSION
public static final ProgramSVSort SIMPLEJAVALONGEXPRESSION
public static final ProgramSVSort SIMPLEJAVABYTESHORTEXPRESSION
public static final ProgramSVSort SIMPLEJAVABYTESHORTINTEXPRESSION
public static final ProgramSVSort SIMPLEANYJAVATYPEEXPRESSION
public static final ProgramSVSort SIMPLEANYJAVANUMBERTYPEEXPRESSION
public static final ProgramSVSort SIMPLEJAVASHORTINTLONGEXPRESSION
public static final ProgramSVSort SIMPLEJAVAINTLONGEXPRESSION
public static final ProgramSVSort SIMPLEJAVACHARBYTESHORTINTEXPRESSION
public static final ProgramSVSort SIMPLEJAVABIGINTEXPRESSION
public static final ProgramSVSort SIMPLEANYNUMBERTYPEEXPRESSION
public static final ProgramSVSort SIMPLEJAVABOOLEANEXPRESSION
public static final ProgramSVSort SIMPLESTRINGEXPRESSION
public static final ProgramSVSort SIMPLENONSTRINGOBJECTEXPRESSION
public static final ProgramSVSort LOOPINIT
public static final ProgramSVSort GUARD
public static final ProgramSVSort FORUPDATES
public static final ProgramSVSort FORLOOP
public static final ProgramSVSort MULTIPLEVARDECL
public static final ProgramSVSort ARRAYPOSTDECL
public static final ProgramSVSort SWITCH
public static final ProgramSVSort CONSTANT_PRIMITIVE_TYPE_VARIABLE
public static final ProgramSVSort CONSTANT_STRING_VARIABLE
public static final ProgramSVSort VARIABLEINIT
public static final ProgramSVSort NONSTRINGLITERAL
public static final ProgramSVSort STRINGLITERAL
public static final ProgramSVSort ARRAYLENGTH
public static final ProgramSVSort EXECUTIONCONTEXT
public ProgramSVSort(Name name)
public boolean canStandFor(Term t)
public boolean canStandFor(ProgramElement check, ExecutionContext ec, Services services)
protected abstract boolean canStandFor(ProgramElement check, Services services)
public ProgramSVSort createInstance(java.lang.String parameter)
static boolean methodConstrReference(ProgramElement pe)
public ProgramElement getSVWithSort(ExtList l, java.lang.Class<?> alternative)
static KeYJavaType getKeYJavaType(ProgramElement pe, ExecutionContext ec, Services services)
static boolean implicit(ProgramElement pe)
public static java.util.Map<Name,ProgramSVSort> name2sort()