escjava.translate
Class ErrorMsg

java.lang.Object
  escjava.translate.ErrorMsg

public final class ErrorMsg

extends java.lang.Object

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

assocDeclClipPolicy

private static final AssocDeclClipPolicy assocDeclClipPolicy

Constructor Detail

ErrorMsg

public ErrorMsg()

Method Detail

print

public 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. Error messages are printed to out.

printSeparatorLine

public static void printSeparatorLine(java.io.PrintStream out)

isErrorLabel

private static boolean isErrorLabel(java.lang.String s)

Returns whether or not 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.

isTraceLabel

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. Requires s to be a label output by an ESC/Java run of Simplify.

printErrorMessage

private static void printErrorMessage(java.lang.String s,
                                      SList counterexampleContext,
                                      RoutineDecl rd,
                                      Set directTargets,
                                      java.io.PrintStream out,
                                      boolean assocOnly)
                               throws SExpTypeError

Parses s and prints a nice error message to out.

Throws:

SExpTypeError

chkToMsg

private static java.lang.String chkToMsg(int tag,
                                         boolean hasAssocDecl)

sortTraceLabels

private static void sortTraceLabels(java.lang.String[] labels,
                                    int size)

Sort the trace labels. Labels are assumed to have the form trace.Name^n,r.c[#i] Here [] denotes optional (zero or one occurrence), n is an ordering number used for the sorting, r is a row number, c is a column number, and i is an iteration number within a loop. Only n is used for sorting; the rest are only for printing purposes.

printTraceInfo

private static void printTraceInfo(java.lang.String s,
                                   java.io.PrintStream out)

Parses s and prints execution trace information to out.

getLoc

private static int getLoc(java.lang.String s,
                          int k)

Converts string s, beginning at index k, into a location.

toNumber

private static int toNumber(java.lang.String s,
                            int k)

Converts the substring beginning at k of s into a number.

displayInvariantContext

private static void displayInvariantContext(SList counterexampleContext,
                                            java.io.PrintStream out)
                                     throws SExpTypeError

Throws:

SExpTypeError

pruneCC

private static SList pruneCC(SList cc)
                      throws SExpTypeError

Prune out s-expressions from the counterexample context that are almost certainly irrelevant.

Throws:

SExpTypeError

declToFileLocStr

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. fileNames is the CorrelatedReader file mappings.

useToFileLocStr

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. fileNames is the CorrelatedReader file mappings.

houdiniPrint

public static void houdiniPrint(java.lang.String label,
                                java.io.PrintStream out,
                                java.lang.String[] fileNames)

Prints a houdini error message to out.

houdiniPrintErrorMessage

private static void houdiniPrintErrorMessage(java.lang.String s,
                                             java.io.PrintStream out,
                                             java.lang.String[] map)
                                      throws SExpTypeError

Parses s and prints an error message for the houdini log to out.

Throws:

SExpTypeError