public final class MiscTools
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private static class |
MiscTools.ReadPVCollector |
private static class |
MiscTools.WrittenAndDeclaredPVCollector |
Modifier | Constructor and Description |
---|---|
private |
MiscTools() |
Modifier and Type | Method and Description |
---|---|
static <S,T,U> java.util.Map<S,U> |
apply(java.util.Map<S,? extends T> m0,
java.util.Map<T,U> m1)
Combine two maps by function application.
|
static ImmutableSet<Pair<Sort,IObserverFunction>> |
collectObservers(Term t)
Recursively collect all observers for this term including all of its sub terms.
|
static <S,T extends S> |
concat(S[] s1,
T[] s2)
Concatenates two arrays.
|
static boolean |
containsWholeWord(java.lang.String s,
java.lang.String word)
Checks whether a string contains another one as a whole word (i.e., separated by
white spaces or a semicolon at the end).
|
(package private) static java.util.List<java.lang.String> |
disectFilename(java.lang.String filename)
Separates the single directory entries in a filename.
|
static <T> boolean |
equalsOrNull(T a,
java.lang.Object... bs)
true iff all are null or a.equals(b)
with equals from type T for every b . |
static <T> boolean |
equalsOrNull(T a,
java.lang.Object b)
true iff both are null or a.equals(b)
with equals from type T. |
static java.lang.String |
filterAlphabetic(java.lang.String string)
Takes a string and returns a string which is potentially shorter and contains a
sub-collection of the original characters.
|
static ImmutableList<Term> |
filterOutDuplicates(ImmutableList<Term> localIns,
ImmutableList<Term> localOuts) |
static ProgramVariable |
findActualVariable(ProgramVariable originalVar,
Node node)
Returns the actual variable for a given one (this means it returns the renamed variable).
|
static OneStepSimplifier |
findOneStepSimplifier(Profile profile)
Returns the
OneStepSimplifier used in the given Profile . |
static OneStepSimplifier |
findOneStepSimplifier(Proof proof)
Returns the
OneStepSimplifier used in the given Proof . |
static java.util.HashMap<java.lang.String,java.lang.String> |
getDefaultTacletOptions()
Returns the default taclet options.
|
static ImmutableSet<ProgramVariable> |
getLocalIns(ProgramElement pe,
Services services)
All variables read in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
getLocallyDeclaredVars(ProgramElement pe,
Services services)
All variables newly declared in the specified program element.
|
static ImmutableSet<ProgramVariable> |
getLocalOuts(ProgramElement pe,
Services services)
All variables changed in the specified program element, excluding newly declared variables.
|
static ImmutableSet<ProgramVariable> |
getLocalOutsAndDeclared(ProgramElement pe,
Services services)
All variables changed in the specified program element, including newly declared variables.
|
static java.lang.String |
getRuleDisplayName(Node node)
Returns the display name of the applied rule in the given
Node of the proof tree in
KeY. |
static java.lang.String |
getRuleDisplayName(RuleApp ruleApp)
Returns the display name of the
RuleApp . |
static java.lang.String |
getRuleName(Node node)
Returns the name of the applied rule in the given
Node of the proof tree in KeY. |
static java.lang.String |
getRuleName(RuleApp ruleApp)
Returns the name of the
RuleApp . |
static ProgramVariable |
getSelf(MethodFrame mf) |
static Term |
getSelfTerm(MethodFrame mf,
Services services)
Returns the receiver term of the passed method frame, or null if the frame belongs to a
static method.
|
static java.lang.String |
getSourcePath(PositionInfo posInfo)
Returns the path to the source file defined by the given
PositionInfo . |
static boolean |
isJMLComment(java.lang.String comment)
There are different kinds of JML markers.
|
static java.lang.String |
join(java.lang.Iterable<?> collection,
java.lang.String delimiter)
Join the string representations of a collection of objects into onw string.
|
static java.lang.String |
join(java.lang.Object[] collection,
java.lang.String delimiter)
Join the string representations of an array of objects into one string.
|
static java.lang.String |
makeFilenameRelative(java.lang.String origFilename,
java.lang.String toFilename)
Returns a filename relative to another one.
|
private static java.lang.String[] |
removeDotDot(java.lang.String[] a) |
static java.lang.String |
toString(java.io.InputStream is)
read an input stream to its end into a string.
|
static ImmutableList<Term> |
toTermList(java.lang.Iterable<ProgramVariable> list,
TermBuilder tb) |
static java.lang.String |
toValidFileName(java.lang.String s) |
static Name |
toValidTacletName(java.lang.String s) |
static Name |
toValidVariableName(java.lang.String s) |
public static ProgramVariable getSelf(MethodFrame mf)
public static Term getSelfTerm(MethodFrame mf, Services services)
mf
- a method frame.services
- services.public static ImmutableSet<ProgramVariable> getLocalIns(ProgramElement pe, Services services)
pe
- a program element.services
- services.public static ImmutableSet<ProgramVariable> getLocalOuts(ProgramElement pe, Services services)
pe
- a program element.services
- services.public static ImmutableSet<ProgramVariable> getLocalOutsAndDeclared(ProgramElement pe, Services services)
pe
- a program element.services
- services.public static ImmutableSet<ProgramVariable> getLocallyDeclaredVars(ProgramElement pe, Services services)
pe
- a program element.services
- services.public static ImmutableSet<Pair<Sort,IObserverFunction>> collectObservers(Term t)
t
- the term for which we want to collect the observer functions.public static <T> boolean equalsOrNull(T a, java.lang.Object b)
true
iff both are null
or a.equals(b)
with equals
from type T.T
- type of a
and result value.a
- an object.b
- another object.true
iff both are null
or a.equals(b)
with equals
from type T.public static <T> boolean equalsOrNull(T a, java.lang.Object... bs)
true
iff all are null
or a.equals(b)
with equals
from type T for every b
.T
- type of a
and result value.a
- an object.bs
- other object.true
iff all are null
or a.equals(b)
with equals
from type T for every b
.public static <S,T extends S> S[] concat(S[] s1, T[] s2)
S
- type o array s1
and of result array.T
- type of array s2
.s1
- an array.s2
- another array.public static <S,T,U> java.util.Map<S,U> apply(java.util.Map<S,? extends T> m0, java.util.Map<T,U> m1)
m0
which are not keys of
m1
are dropped. This implementation tries to use the same implementation of
Map
(provided in Java SE) as m0
.S
- type of m0
.T
- type of m1
.U
- new type of result map indexes.m0
- a map.m1
- another map.static java.util.List<java.lang.String> disectFilename(java.lang.String filename)
filename
- a file name.public static java.lang.String makeFilenameRelative(java.lang.String origFilename, java.lang.String toFilename)
origFilename
- a filename.toFilename
- the name of a parent directory of origFilename
.origFilename
relative to toFilename
private static java.lang.String[] removeDotDot(java.lang.String[] a)
public static Name toValidTacletName(java.lang.String s)
public static java.lang.String toValidFileName(java.lang.String s)
public static Name toValidVariableName(java.lang.String s)
public static java.lang.String join(java.lang.Iterable<?> collection, java.lang.String delimiter)
Object.toString()
is used to turn the objects into strings.collection
- an arbitrary non-null collectiondelimiter
- a non-null string which is put between the elements.public static java.lang.String join(java.lang.Object[] collection, java.lang.String delimiter)
Object.toString()
is used to turn the objects into strings.collection
- an arbitrary non-null array of objectsdelimiter
- a non-null string which is put between the elements.public static java.lang.String filterAlphabetic(java.lang.String string)
string
- an arbitrary stringpublic static boolean containsWholeWord(java.lang.String s, java.lang.String word)
s
- string to search inword
- string to be searched forpublic static boolean isJMLComment(java.lang.String comment)
comment
- public static java.lang.String getRuleDisplayName(Node node)
Returns the display name of the applied rule in the given Node
of the proof tree in
KeY.
This method is required for the symbolic execution tree extraction, e.g. used in the Symbolic Execution Tree Debugger.
public static java.lang.String getRuleDisplayName(RuleApp ruleApp)
Returns the display name of the RuleApp
.
This method is required for the symbolic execution tree extraction, e.g. used in the Symbolic Execution Tree Debugger.
public static java.lang.String getRuleName(Node node)
Returns the name of the applied rule in the given Node
of the proof tree in KeY.
This method is required for the symbolic execution tree extraction, e.g. used in the Symbolic Execution Tree Debugger.
public static java.lang.String getRuleName(RuleApp ruleApp)
Returns the name of the RuleApp
.
This method is required for the symbolic execution tree extraction, e.g. used in the Symbolic Execution Tree Debugger.
public static OneStepSimplifier findOneStepSimplifier(Proof proof)
OneStepSimplifier
used in the given Proof
.proof
- The Proof
to get its used OneStepSimplifier
.OneStepSimplifier
or null
if not available.public static OneStepSimplifier findOneStepSimplifier(Profile profile)
OneStepSimplifier
used in the given Profile
.profile
- The Profile
to get its used OneStepSimplifier
.OneStepSimplifier
or null
if not available.public static ProgramVariable findActualVariable(ProgramVariable originalVar, Node node)
node
- the Node where to look up the actual variable (result from renaming)public static ImmutableList<Term> toTermList(java.lang.Iterable<ProgramVariable> list, TermBuilder tb)
public static java.lang.String toString(java.io.InputStream is) throws java.io.IOException
is
- a non-null open input streamjava.io.IOException
- may occur while reading the streampublic static ImmutableList<Term> filterOutDuplicates(ImmutableList<Term> localIns, ImmutableList<Term> localOuts)
public static java.util.HashMap<java.lang.String,java.lang.String> getDefaultTacletOptions()
public static java.lang.String getSourcePath(PositionInfo posInfo)
PositionInfo
.posInfo
- The PositionInfo
to extract source file from.null
if not available.