Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

## 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`

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

The ESC/Java2 Project Homepage