|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.translate.ErrorMsg
Provides printing of error messages to the user.
Field Summary | |
private static AssocDeclClipPolicy |
assocDeclClipPolicy
|
Constructor Summary | |
ErrorMsg()
|
Method Summary | |
private static java.lang.String |
chkToMsg(int tag,
boolean hasAssocDecl)
|
private static java.lang.String |
declToFileLocStr(java.lang.String loc,
java.lang.String[] fileNames)
return the string rep of the location loc when it is used as an associated decl location. |
private static void |
displayInvariantContext(SList counterexampleContext,
java.io.PrintStream out)
|
private static int |
getLoc(java.lang.String s,
int k)
Converts string s , beginning at index k ,
into a location. |
static void |
houdiniPrint(java.lang.String label,
java.io.PrintStream out,
java.lang.String[] fileNames)
Prints a houdini error message to out. |
private static void |
houdiniPrintErrorMessage(java.lang.String s,
java.io.PrintStream out,
java.lang.String[] map)
Parses s and prints an error message for the
houdini log to out. |
private static boolean |
isErrorLabel(java.lang.String s)
Returns whether or not s is string that indicates
which ESC/Java check the program violates.
|
(package private) static boolean |
isTraceLabel(java.lang.String s)
Returns whether or not s is string that indicates
information about the execution trace in the counterexample
context.
|
static void |
print(java.lang.String name,
SList labelList,
SList counterexampleContext,
RoutineDecl rd,
Set directTargets,
java.io.PrintStream out)
Prints an error message for proof obligation name ,
where labelList and
counterexampleContext are labels and
counterexample from Simplify. |
private static void |
printErrorMessage(java.lang.String s,
SList counterexampleContext,
RoutineDecl rd,
Set directTargets,
java.io.PrintStream out,
boolean assocOnly)
Parses s and prints a nice error message to
out . |
static void |
printSeparatorLine(java.io.PrintStream out)
|
private static void |
printTraceInfo(java.lang.String s,
java.io.PrintStream out)
Parses s and prints execution trace information to
out . |
private static SList |
pruneCC(SList cc)
Prune out s-expressions from the counterexample context that are almost certainly irrelevant. |
private static void |
sortTraceLabels(java.lang.String[] labels,
int size)
Sort the trace labels. |
private static int |
toNumber(java.lang.String s,
int k)
Converts the substring beginning at k of s
into a number. |
private static java.lang.String |
useToFileLocStr(java.lang.String loc,
java.lang.String[] fileNames)
return the string rep of the location loc when it is used as a use. |
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
private static final AssocDeclClipPolicy assocDeclClipPolicy
Constructor Detail |
public ErrorMsg()
Method Detail |
public static void print(java.lang.String name, SList labelList, SList counterexampleContext, RoutineDecl rd, Set directTargets, java.io.PrintStream out)
name
,
where labelList
and
counterexampleContext
are labels and
counterexample from Simplify. Error messages are printed to
out
.
public static void printSeparatorLine(java.io.PrintStream out)
private static boolean isErrorLabel(java.lang.String s)
s
is string that indicates
which ESC/Java check the program violates.
Requires s
to be a label output by an ESC/Java run
of Simplify.
static boolean isTraceLabel(java.lang.String s)
s
is string that indicates
information about the execution trace in the counterexample
context.
Requires s
to be a label output by an ESC/Java
run of Simplify.
private static void printErrorMessage(java.lang.String s, SList counterexampleContext, RoutineDecl rd, Set directTargets, java.io.PrintStream out, boolean assocOnly) throws SExpTypeError
s
and prints a nice error message to
out
.
SExpTypeError
private static java.lang.String chkToMsg(int tag, boolean hasAssocDecl)
private static void sortTraceLabels(java.lang.String[] labels, int size)
private static void printTraceInfo(java.lang.String s, java.io.PrintStream out)
s
and prints execution trace information to
out
.
private static int getLoc(java.lang.String s, int k)
s
, beginning at index k
,
into a location.
private static int toNumber(java.lang.String s, int k)
k
of s
into a number.
private static void displayInvariantContext(SList counterexampleContext, java.io.PrintStream out) throws SExpTypeError
SExpTypeError
private static SList pruneCC(SList cc) throws SExpTypeError
SExpTypeError
private static java.lang.String declToFileLocStr(java.lang.String loc, java.lang.String[] fileNames)
private static java.lang.String useToFileLocStr(java.lang.String loc, java.lang.String[] fileNames)
public static void houdiniPrint(java.lang.String label, java.io.PrintStream out, java.lang.String[] fileNames)
private static void houdiniPrintErrorMessage(java.lang.String s, java.io.PrintStream out, java.lang.String[] map) throws SExpTypeError
s
and prints an error message for the
houdini log to out.
SExpTypeError
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |