public final class MiscTools
extends java.lang.Object
Modifier and Type | Method and Description |
---|---|
static java.util.List<LocationVariable> |
applicableHeapContexts(Modality modality,
Services services)
Returns the applicable heap contexts out of the currently available set
of three contexts: The normal heap, the saved heap (transaction), and the
permission heap.
|
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).
|
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)
Deprecated.
|
static java.net.URI |
extractURI(DataLocation loc)
Tries to extract a valid URI from the given DataLocation.
|
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 java.util.Optional<LoopSpecification> |
getSpecForTermWithLoopStmt(Term loopTerm,
Services services)
Returns the
LoopSpecification for the program in the given term,
the active statement of which has to be a loop statement. |
static java.net.URI |
getZipEntryURI(java.util.zip.ZipFile zipFile,
java.lang.String entryName)
Creates a URI (that contains a URL) pointing to the entry with the given name inside
the given zip file.
|
static boolean |
isJMLComment(java.lang.String comment)
There are different kinds of JML markers.
|
static boolean |
isPermissions(Services services) |
static boolean |
isTransaction(Modality modality)
Checks whether the given
Modality is a transaction modality. |
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.
|
static java.net.URL |
parseURL(java.lang.String input)
This method is the central place for parsing a URL from a String.
|
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 java.util.Optional<LoopSpecification> getSpecForTermWithLoopStmt(Term loopTerm, Services services)
LoopSpecification
for the program in the given term,
the active statement of which has to be a loop statement. Returns an
empty Optional
if there is no specification for that statement.
Asserts that there is indeed a Java block in the term which has as active
statement a loop statement, thus throws an AssertionError
if not
or otherwise results in undefined behavior in that case.loopTerm
- The term for which to return the LoopSpecification
.localSpecRepo
- TODOLoopSpecification
for the loop statement in the given
term or an empty optional if there is no specified invariant for the
loop.public static boolean isPermissions(Services services)
public static boolean isTransaction(Modality modality)
Modality
is a transaction modality.modality
- The modality to check.Modality
is a transaction modality.public static java.util.List<LocationVariable> applicableHeapContexts(Modality modality, Services services)
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.@Deprecated public static <T> boolean equalsOrNull(T a, java.lang.Object b)
null
or a.equals(b)
with equals
from type T.
You should use Objects.equals(Object, Object)
directly.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.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
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.public static java.net.URI extractURI(DataLocation loc)
loc
- the given DataLocationpublic static java.net.URI getZipEntryURI(java.util.zip.ZipFile zipFile, java.lang.String entryName) throws java.io.IOException
URI
supports RFC 3986
(currently, as of 02-2020, it seems like there are no plans for this).zipFile
- the given zipentryName
- the entry path relative to the root of the zipjava.io.IOException
- if an I/O error occurspublic static java.net.URL parseURL(java.lang.String input) throws java.net.MalformedURLException
Paths.get(String, String...)
.input
- the String to convertjava.net.MalformedURLException
- if the string can not be converted to URL because of an
unknown protocol or illegal formatCopyright © 2003-2019 The KeY-Project.