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

escjava.translate
Class ErrorMsg

java.lang.Object
  extended byescjava.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

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

The ESC/Java2 Project Homepage