public final class MiscTools extends Object
Modifier and Type | Class and Description |
---|---|
private static class |
MiscTools.ReadPVCollector |
private static class |
MiscTools.WrittenPVCollector |
Modifier | Constructor and Description |
---|---|
private |
MiscTools() |
Modifier and Type | Method and Description |
---|---|
static <S,T,U> Map<S,U> |
apply(Map<S,? extends T> m0,
Map<T,U> m1)
Combine two maps by function application.
|
static ImmutableSet<Pair<Sort,IObserverFunction>> |
collectObservers(Term t) |
static <S,T extends S> |
concat(S[] s1,
T[] s2)
Concatenates two arrays.
|
static boolean |
containsWholeWord(String s,
String word)
Checks whether a string contains another one as a whole word
(i.e., separated by whitespaces or a semicolon at the end).
|
(package private) static List<String> |
disectFilename(String filename)
Separates the single directory entries in a filename.
|
static <T> boolean |
equalsOrNull(T a,
Object... bs) |
static <T> boolean |
equalsOrNull(T a,
Object b)
True if both are
null or a.equals(b) with equals from type T. |
static String |
filterAlphabetic(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 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 HashMap<String,String> |
getDefaultTacletOptions()
Returns the default taclet options.
|
static ImmutableSet<ProgramVariable> |
getLocalIns(ProgramElement pe,
Services services) |
static ImmutableSet<ProgramVariable> |
getLocalOuts(ProgramElement pe,
Services services) |
static String |
getRuleDisplayName(Node node)
Returns the display name of the applied rule in the given
Node of
the proof tree in KeY. |
static String |
getRuleDisplayName(RuleApp ruleApp)
Returns the display name of the
RuleApp . |
static String |
getRuleName(Node node)
Returns the name of the applied rule in the given
Node of
the proof tree in KeY. |
static 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 String |
getSourcePath(PositionInfo posInfo)
Returns the path to the source file defined by the given
PositionInfo . |
static boolean |
isJMLComment(String comment)
There are different kinds of JML markers.
|
static String |
join(Iterable<?> collection,
String delimiter)
Join the string representations of a collection of objects into onw
string.
|
static String |
join(Object[] collection,
String delimiter)
Join the string representations of an array of objects into one
string.
|
static String |
makeFilenameRelative(String origFilename,
String toFilename)
Returns a filename relative to another one.
|
private static String[] |
removeDotDot(String[] a) |
static String |
toString(InputStream is)
read an input stream to its end into a string.
|
static ImmutableList<Term> |
toTermList(Iterable<ProgramVariable> list,
TermBuilder tb) |
static String |
toValidFileName(String s) |
static Name |
toValidTacletName(String s) |
static Name |
toValidVariableName(String s) |
public static ProgramVariable getSelf(MethodFrame mf)
public static Term getSelfTerm(MethodFrame mf, Services services)
public static ImmutableSet<ProgramVariable> getLocalIns(ProgramElement pe, Services services)
public static ImmutableSet<ProgramVariable> getLocalOuts(ProgramElement pe, Services services)
public static ImmutableSet<Pair<Sort,IObserverFunction>> collectObservers(Term t)
public static <T> boolean equalsOrNull(T a, Object b)
null
or a.equals(b)
with equals
from type T.public static <T> boolean equalsOrNull(T a, Object... bs)
public static <S,T extends S> S[] concat(S[] s1, T[] s2)
public static <S,T,U> Map<S,U> apply(Map<S,? extends T> m0, 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
.static List<String> disectFilename(String filename)
public static String makeFilenameRelative(String origFilename, String toFilename)
public static String join(Iterable<?> collection, 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 String join(Object[] collection, 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 String filterAlphabetic(String string)
string
- an arbitrary stringpublic static boolean containsWholeWord(String s, String word)
s
- string to search inword
- string to be searched forpublic static boolean isJMLComment(String comment)
comment
- public static 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 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 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 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 ImmutableList<Term> toTermList(Iterable<ProgramVariable> list, TermBuilder tb)
public static String toString(InputStream is) throws IOException
is
- a non-null open input streamIOException
- may occur while reading the streampublic static ImmutableList<Term> filterOutDuplicates(ImmutableList<Term> localIns, ImmutableList<Term> localOuts)
public static HashMap<String,String> getDefaultTacletOptions()
public static String getSourcePath(PositionInfo posInfo)
PositionInfo
.posInfo
- The PositionInfo
to extract source file from.null
if not available.