    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.translate;
    004
    005    import java.io.*;
    006
    007    import javafe.util.Assert;
    008    import javafe.util.Info;
    009    import javafe.util.ErrorSet;
    010    import javafe.util.Location;
    011    import javafe.util.Set;
    012
    013    import javafe.ast.RoutineDecl;
    014
    015    import escjava.Main;
    016    import escjava.prover.*;
    017    import escjava.ast.TagConstants;
    018
    019
    020    /**
    021     * Provides printing of error messages to the user.
    022     */
    023
    024    public final class ErrorMsg
    025    {
    026        /**
    027         * Prints an error message for proof obligation <code>name</code>,
    028         * where <code>labelList</code> and
    029         * <code>counterexampleContext</code> are labels and
    030         * counterexample from Simplify.  Error messages are printed to
    031         * <code>out</code>.
    032         */
    033        public static void print(String name,
    034                                 SList labelList,
    035                                 SList counterexampleContext,
    036                                 /*@ non_null */ RoutineDecl rd,
    037                                 /*@ non_null */ Set directTargets,
    038                                 /*@ non_null */ PrintStream out) {
    039            try {
    040                int cLabels = labelList.length();
    041                int iErrorLabel = -1;
    042                String tail = null;
    043                for (int i = 0; i < cLabels; i++) {
    044                    String s = labelList.at(i).getAtom().toString();
    045                    if (isErrorLabel(s)) {
    046                        printErrorMessage(s, counterexampleContext, rd, directTargets, out, false);
    047                        iErrorLabel = i;
    048                        int j = s.indexOf('@');
    049                        if (j != -1) tail = s.substring(j);
    050                        break;
    051                    }
    052                }
    053                if (iErrorLabel == -1) {
    054                    //@ unreachable;
    055                    StringBuffer s = new StringBuffer("Unknown cause!  Labels are");
    056                    for (int i = 0; i < cLabels; i++) {
    057                         s.append(" " + labelList.at(i).getAtom().toString());
    058                    }
    059                    ErrorSet.error(s.toString());
    060                }
    061
    062                // print the execution trace info if requested
    063                if (Main.options().traceInfo > 0) {
    064                    // copy the trace labels to a String array
    065                    String traceLabels[] = new String[cLabels];
    066                    int index = 0;
    067                    for (int i = 0; i < cLabels; i++) {
    068                        String s = labelList.at(i).getAtom().toString();
    069                        if (isTraceLabel(s)) {
    070                            traceLabels[index] = s.substring(6);
    071                            index++;
    072                        }
    073                    }
    074                    if (index > 0) {
    075                        sortTraceLabels(traceLabels, index);
    076                        out.println("Execution trace information:");
    077                        for (int i = 0; i < index; i++)
    078                            printTraceInfo(traceLabels[i], out);
    079                        System.out.println();
    080                    }
    081                }
    082
    083                if (Main.options().counterexample) {
    084                    out.println("Counterexample context:");
    085                    SList prunedCC = pruneCC(counterexampleContext);
    086                    int n = prunedCC.length();
    087                    for (int i = 0; i < n; i++) {
    088                        out.print("    ");
    089                        prunedCC.at(i).prettyPrint(out);
    090                        out.println();
    091                    }
    092                    out.println();
    093                }
    094
    095                if (Info.on || Main.options().pcc) {
    096                    Assert.notFalse(counterexampleContext.length() > 1 &&
    097                                    counterexampleContext.at(0).toString().equals("AND"));
    098                    out.println("Full counterexample context:");
    099                    int n = counterexampleContext.length();
    100                    for (int i = 2; i < n; i++) {
    101                        out.print("    ");
    102                        counterexampleContext.at(i).print(out);
    103                        out.println();
    104                    }
    105                }
    106
    107                boolean userLabels = false;
    108                for (int i = 0; i < cLabels; i++) {
    109                    String label = labelList.at(i).getAtom().toString();
    110                    if (i == iErrorLabel || label.startsWith("vc.") ||
    111                        (Main.options().traceInfo > 0 && isTraceLabel(label))) {
    112                        continue;
    113                    }
    114                    if (tail != null && label.endsWith(tail)) {
    115                        printErrorMessage(label, counterexampleContext, rd, directTargets, out, true);
    116                        continue;
    117                    }
    118                    if (label.startsWith("AdditionalInfo")) {
    119
    120                        printErrorMessage(label, counterexampleContext, rd, directTargets, out, true);
    121                        continue;
    122
    123                    }
    124                    if (!userLabels) {
    125                        out.println("Counterexample labels:");
    126                        userLabels = true;
    127                    }
    128                    out.print("    " + label);
    129                }
    130                if (userLabels) {
    131                    out.println();
    132                    out.println();
    133                }
    134            } catch (escjava.prover.SExpTypeError s) {
    135                Assert.fail("unexpected S-expression exception");
    136            }
    137            printSeparatorLine(out);
    138        }
    139
    140        public static void printSeparatorLine(/*@ non_null */ PrintStream out) {
    141            if (!Main.options().quiet) {
    142                out.println("------------------------------------------------------------------------");
    143            }
    144        }
    145
    146        /**
    147         * Returns whether or not <code>s</code> is string that indicates
    148         * which ESC/Java check the program violates.
    149         *
    150         * Requires <code>s</code> to be a label output by an ESC/Java run
    151         * of Simplify.
    152         */
    153
    154        private static boolean isErrorLabel(String s) {
    155            if (s.equals("Inconsistent")) return true;
    156            return s.indexOf('@') != -1;
    157        }
    158
    159
    160        /**
    161         * Returns whether or not <code>s</code> is string that indicates
    162         * information about the execution trace in the counterexample
    163         * context.
    164         *
    165         * Requires <code>s</code> to be a label output by an ESC/Java
    166         * run of Simplify.
    167         */
    168
    169        static boolean isTraceLabel(/*@ non_null */ String s) {
    170            return s.startsWith("trace.");
    171        }
    172
    173
    174        /** Parses <code>s</code> and prints a nice error message to
    175         * <code>out</code>.
    176         **/
    177
    178        private static void printErrorMessage(String s,
    179                                              SList counterexampleContext,
    180                                              /*@ non_null */ RoutineDecl rd,
    181                                              /*@ non_null */ Set directTargets,
    182                                              /*@ non_null */ PrintStream out,
    183                                              boolean assocOnly)
    184            throws SExpTypeError {
    185
    186          try {
    187            if (counterexampleContext == null) {
    188                counterexampleContext = SList.make();
    189            }
    190
    191            int k = s.indexOf('@');
    192            //Assert.notFalse(k != -1 || assocOnly);
    193            int locUse = 0;
    194            if (k != -1) {
    195                locUse = getLoc(s, k+1);
    196                s = s.substring(0, k);
    197            }
    198
    199            boolean hasAssocDecl = false;
    200            int locDecl =  Location.NULL;
    201            int locAux = Location.NULL;
    202            k = s.lastIndexOf(':');
    203            if (k != -1) {
    204                hasAssocDecl = true;
    205                locDecl = getLoc(s, k+1);
    206                s = s.substring(0, k);
    207            }
    208
    209            k = s.lastIndexOf(':');
    210            if (k != -1) {
    211                locAux = locDecl;
    212                locDecl = getLoc(s, k+1);
    213                s = s.substring(0, k);
    214            }
    215
    216            k = s.indexOf('/');
    217            int auxID = -1;  // -1 means none
    218            if (k != -1) {
    219                auxID = toNumber(s, k+1);
    220                s = s.substring(0, k);
    221            }
    222
    223            int tag = TagConstants.checkFromString(s);
    224            String msg = chkToMsg( tag, hasAssocDecl );
    225            if (msg == null) return;
    226
    227            if (locUse != Location.NULL) ErrorSet.warning( locUse,
    228                              msg+" (" + TagConstants.toString(tag) + ")" );
    229            else if (tag != TagConstants.CHKADDINFO)
    230                    ErrorSet.warning( msg+" (" + TagConstants.toString(tag) + ")" );
    231
    232            if( locDecl != Location.NULL) {
    233                ErrorSet.getReporter().reportAssociatedInfo2(locDecl, assocDeclClipPolicy);
    234                if (!Location.isWholeFileLoc(locDecl)) {
    235                    //System.out.println("Associated declaration is "
    236                    //             + Location.toString(locDecl) + ":");
    237                    //ErrorSet.displayColumn(locDecl, assocDeclClipPolicy);
    238                } else {
    239                    //System.out.println("Associated declaration is "
    240                    //             + Location.toString(locDecl) );
    241                }
    242            }
    243
    244            if( locAux != Location.NULL) {
    245                ErrorSet.getReporter().reportAssociatedInfo2(locAux, assocDeclClipPolicy);
    246                if (!Location.isWholeFileLoc(locAux)) {
    247                    //System.out.println("Associated declaration is "
    248                    //             + Location.toString(locAux) + ":");
    249                    //ErrorSet.displayColumn(locAux, assocDeclClipPolicy);
    250                } else {
    251                    //System.out.println("Associated declaration is "
    252                    //             + Location.toString(locAux) );
    253                }
    254            }
    255
    256            switch (tag) {
    257            case TagConstants.CHKLOOPOBJECTINVARIANT:
    258            case TagConstants.CHKOBJECTINVARIANT:
    259                displayInvariantContext(counterexampleContext, out);
    260            }
    261
    262            if (Main.options().suggest) {
    263                Object auxInfo;
    264                if (auxID == -1) {
    265                    auxInfo = null;
    266                } else {
    267                    auxInfo = AuxInfo.get(auxID);
    268                }
    269                String sug = Suggestion.generate(tag, auxInfo, rd, directTargets,
    270                                                 counterexampleContext, locDecl);
    271                if (sug == null) {
    272                    sug = "none";
    273                }
    274                System.out.println("Suggestion [" + Location.toLineNumber(locUse)+
    275                                   "," + Location.toColumn(locUse) + "]: " + sug);
    276            }
    277          } catch (javafe.util.AssertionFailureException e) {
    278            System.out.println("FAILED TO PRINT ERROR MESSAGE FOR " + s);
    279            throw e;
    280          }
    281        }
    282
    283
    284
    285
    286        private static final AssocDeclClipPolicy assocDeclClipPolicy =
    287            new AssocDeclClipPolicy();
    288
    289
    290        private static String chkToMsg( int tag, boolean hasAssocDecl ) {
    291            String r = null;
    292            // Finally, describe the error
    293            switch (tag) {
    294            case TagConstants.CHKARITHMETIC:
    295                r = ("Possible division by zero");
    296                Assert.notFalse(!hasAssocDecl);
    297                break;
    298            case TagConstants.CHKARRAYSTORE:
    299                r = ("Type of right-hand side possibly not a subtype of " +
    300                     "array element type");
    301                Assert.notFalse(!hasAssocDecl);
    302                break;
    303            case TagConstants.CHKASSERT:
    304                r = ("Possible assertion failure");
    305                Assert.notFalse(!hasAssocDecl);
    306                break;
    307            case TagConstants.CHKCLASSCAST:
    308                r = ("Possible type cast error");
    309                Assert.notFalse(!hasAssocDecl);
    310                break;
    311            case TagConstants.CHKCODEREACHABILITY:
    312                r = ("Code marked as unreachable may possibly be reached");
    313                Assert.notFalse(!hasAssocDecl);
    314                break;
    315            case TagConstants.CHKCONSISTENT:
    316                r = ("Possible inconsistent added axiom");
    317                break;
    318            case TagConstants.CHKCONSTRAINT:
    319                r = ("Possible violation of object constraint at exit");
    320                Assert.notFalse(hasAssocDecl);
    321                break;
    322            case TagConstants.CHKDECREASES_BOUND:
    323                r = "Negative loop variant function may not lead to loop exit";
    324                Assert.notFalse(hasAssocDecl);
    325                break;
    326            case TagConstants.CHKDECREASES_DECR:
    327                r = "Loop variant function possible not decreased";
    328                Assert.notFalse(hasAssocDecl);
    329                break;
    330            case TagConstants.CHKDEFINEDNESS:
    331                r = ("Read of variable when its value may be meaningless");
    332                Assert.notFalse(hasAssocDecl);
    333                break;
    334            case TagConstants.CHKINDEXNEGATIVE:
    335                r = ("Possible negative array index");
    336                Assert.notFalse(!hasAssocDecl);
    337                break;
    338            case TagConstants.CHKINDEXTOOBIG:
    339                r = ("Array index possibly too large");
    340                Assert.notFalse(!hasAssocDecl);
    341                break;
    342            case TagConstants.CHKINITIALLY:
    343                r = ("Possible violation of initially condition at constructor exit");
    344                Assert.notFalse(hasAssocDecl);
    345                break;
    346            case TagConstants.CHKLOOPINVARIANT:
    347                r = ("Loop invariant possibly does not hold");
    348                Assert.notFalse(hasAssocDecl);
    349                break;
    350            case TagConstants.CHKLOOPOBJECTINVARIANT:
    351                r = ("Object invariant possibly does not hold on loop boundary");
    352                Assert.notFalse(hasAssocDecl);
    353                break;
    354            case TagConstants.CHKINITIALIZATION:
    355                r = ("Possible dynamic use before meaningful assignment of local " +
    356                     "variable");
    357                Assert.notFalse(hasAssocDecl);
    358                break;
    359            case TagConstants.CHKLOCKINGORDER:
    360                r = ("Possible deadlock");
    361
    362                break;
    363            case TagConstants.CHKMODIFIES:
    364                r = ("Possible violation of modifies clause");
    365                //Assert.notFalse(hasAssocDecl);
    366                break;
    367            case TagConstants.CHKNEGATIVEARRAYSIZE:
    368                r = ("Possible attempt to allocate array of negative length");
    369                Assert.notFalse(!hasAssocDecl);
    370                break;
    371            case TagConstants.CHKNONNULL:
    372                r = ("Possible assignment of null to variable declared non_null");
    373                Assert.notFalse(hasAssocDecl);
    374                break;
    375            case TagConstants.CHKNONNULLINIT:
    376                r = ("Field declared non_null possibly not initialized");
    377                Assert.notFalse(hasAssocDecl);
    378                break;
    379            case TagConstants.CHKNONNULLRESULT:
    380                r = "Method declared non_null may return null";
    381                Assert.notFalse(hasAssocDecl);
    382                break;
    383            case TagConstants.CHKNULLPOINTER:
    384                r = ("Possible null dereference");
    385                Assert.notFalse(!hasAssocDecl);
    386                break;
    387            case TagConstants.CHKOBJECTINVARIANT:
    388                // It would be nice to split this error into two:
    389                //  *  Possible violation of object invariant at end of body (InvPost)
    390                //  *  Possible violation of object invariant before call (InvPre)
    391                r = ("Possible violation of object invariant");
    392                Assert.notFalse(hasAssocDecl);
    393                break;
    394            case TagConstants.CHKOWNERNULL:
    395                r = ("Owner ghost field of constructed object possibly non-null");
    396                Assert.notFalse(!hasAssocDecl);
    397                break;
    398            case TagConstants.CHKPOSTCONDITION:
    399                r = ("Postcondition possibly not established");
    400                Assert.notFalse(hasAssocDecl);
    401                break;
    402            case TagConstants.CHKPRECONDITION:
    403                r = ("Precondition possibly not established");
    404                Assert.notFalse(hasAssocDecl);
    405                break;
    406            case TagConstants.CHKSHARING:
    407                r = ("Possible race condition");
    408                Assert.notFalse(hasAssocDecl);
    409                break;
    410            case TagConstants.CHKSHARINGALLNULL:
    411                r = ("Possible that all monitors are null");
    412                Assert.notFalse(hasAssocDecl);
    413                break;
    414            case TagConstants.CHKWRITABLE:
    415                r = ("Write of variable when disallowed");
    416                Assert.notFalse(hasAssocDecl);
    417                break;
    418            case TagConstants.CHKUNEXPECTEDEXCEPTION:
    419                r = ("Possible unexpected exception");
    420                // "strLocDecl" may or may not be null
    421                break;
    422            case TagConstants.CHKUNEXPECTEDEXCEPTION2:
    423                r = ("Possible exception allowed by the specification (perhaps inherited) but not declared by the method's throws clause");
    424                break;
    425            case TagConstants.CHKCONSTRUCTORLEAK:
    426            case TagConstants.CHKINITIALIZERLEAK:
    427            case TagConstants.CHKUNENFORCEBLEOBJECTINVARIANT:
    428            case TagConstants.CHKWRITABLEDEFERRED:
    429            case TagConstants.CHKMODIFIESEXTENSION:
    430                // this  a syntactic warning, not a semantic check
    431                //@ unreachable;
    432                Assert.fail("unexpected error name tag");
    433                r = TagConstants.toString(tag);
    434                break;
    435            default:
    436                //@ unreachable;
    437                Assert.fail("Bad tag");
    438                break;
    439            case TagConstants.CHKADDINFO:
    440                r = TagConstants.toString(tag);
    441            case TagConstants.CHKQUIET:
    442                break;
    443            }
    444            return r;
    445        }
    446
    447
    448        /** Sort the trace labels.  Labels are assumed to have the form
    449            trace.Name^n,r.c[#i]
    450            Here [] denotes optional (zero or one occurrence), n is an ordering
    451            number used for the sorting, r is a row number, c is a column number, and
    452            i is an iteration number within a loop.  Only n is used for sorting;
    453            the rest are only for printing purposes.
    454        **/
    455        private static void sortTraceLabels(/*@ non_null */ String[] labels,
    456                                            int size) {
    457            // create an array containing the n-value (see comment above) of
    458            // each label
    459            int traceLocs[] = new int[size];
    460            for (int i = 0; i < size; i++) {
    461                int caret = labels[i].indexOf("^");
    462                Assert.notFalse(caret != -1);
    463                int comma = labels[i].indexOf(",");
    464                Assert.notFalse(comma != -1);
    465                Assert.notFalse(caret < comma);
    466                String n = labels[i].substring(caret + 1, comma);
    467                traceLocs[i] = toNumber(n, 0);
    468            }
    469
    470            // bubble sort the labels
    471            int sizeMinusOne = size - 1;
    472            for (int i = 0; i < sizeMinusOne; i++) {
    473                for (int j = sizeMinusOne; i < j; j--) {
    474                    if (traceLocs[j] < traceLocs[j-1]) {
    475                        // swap the j-1 and jth elements in both arrays
    476                        int tempLoc;
    477                        String tempLabel;
    478                        tempLoc = traceLocs[j];
    479                        tempLabel = labels[j];
    480                        traceLocs[j] = traceLocs[j-1];
    481                        labels[j] = labels[j-1];
    482                        traceLocs[j-1] = tempLoc;
    483                        labels[j-1] = tempLabel;
    484                    }
    485                }
    486            }
    487        }
    488
    489
    490        /** Parses <code>s</code> and prints execution trace information to
    491         * <code>out</code>.
    492         **/
    493
    494        private static void printTraceInfo(/*@ non_null */ String s,
    495                                           /*@ non_null */ PrintStream out) {
    496            // first parse the String to get its location (the last row-col pair
    497            //   in its sequence of numbers)
    498            int caret = s.indexOf("^");
    499            Assert.notFalse(caret != -1);
    500            int comma = s.indexOf(",");
    501            Assert.notFalse(comma != -1);
    502            String temp = s.substring(comma + 1);
    503            int hash = temp.indexOf("#");
    504            int iteration = -1;
    505            if (hash != -1) {
    506                iteration = toNumber(temp, hash + 1);
    507                temp = temp.substring(0, hash);
    508            }
    509            int loc = getLoc(temp,0);
    510            String location = Location.toString(loc);
    511
    512            s = s.substring(0,caret);
    513            if (s.equals("RoutineException")) {
    514                out.println("    Routine call returned exceptionally in " +
    515                            location + ".");
    516            } else if (s.equals("FirstOpOnly")) {
    517                out.println("    Short circuited boolean operation in " +
    518                            location + ".");
    519            } else if (s.equals("LoopIter")) {
    520                if (iteration == -1) {
    521                    out.println("    At the top of arbitrary loop iteration at "
    522                                + location + ".");
    523                } else {
    524                    out.println("    Reached top of loop after " + iteration +
    525                                " iteration"
    526                                + (iteration == 1 ? "" : "s") + " in "
    527                                + location + ".");
    528                }
    529            } else if (s.equals("FinallyBegin")) {
    530                out.println("    Abnormal entry to finally clause at " +
    531                            location + ".");
    532            } else if (s.equals("FinallyEnd")) {
    533                out.println("    Resuming abnormal execution path after finally clause at " +
    534                            location + ".");
    535            } else if (s.equals("CallReturn")) {
    536                out.println("    Returned from inlined call at " + location + ".");
    537            } else {
    538                if (s.equals("Then") || s.equals("Else")) {
    539                    s += " branch";
    540                } else if (s.equals("Switch")) {
    541                    s += " case";
    542                } else if (s.equals("ImplicitReturn")) {
    543                    s = "implicit return";
    544                }
    545
    546                out.println("    Executed " + s.toLowerCase() +" in " +
    547                            location + ".");
    548            }
    549        }
    550
    551        /** Converts string <code>s</code>, beginning at index <code>k</code>,
    552         * into a location.
    553         **/
    554
    555        private static int getLoc(String s, int k) {
    556            String suffix = s.substring(k);
    557            return UniqName.suffixToLoc(suffix,true);
    558        }
    559
    560        /** Converts the substring beginning at <code>k</code> of <code>s</code>
    561         * into a number.
    562         **/
    563
    564        private static int toNumber(String s, int k) {
    565            int n = 0;
    566            while (k < s.length()) {
    567                n = 10*n + s.charAt(k) - '0';
    568                k++;
    569            }
    570            return n;
    571        }
    572
    573        private static void displayInvariantContext(/*@ non_null */ SList counterexampleContext,
    574                                                    /*@ non_null */ PrintStream out)
    575            throws SExpTypeError {
    576            if (Main.options().plainWarning)
    577                return;
    578
    579            boolean headerDisplayed = false;
    580
    581            int n = counterexampleContext.length();
    582            for (int i = 0; i < n; i++) {
    583                SExp contextLine = counterexampleContext.at(i);
    584                if (contextLine.toString().indexOf("brokenObj")== -1)
    585                    continue;
    586
    587                if (!headerDisplayed) {
    588                    out.println("Possibly relevant items from the counterexample context:  ");
    589                    headerDisplayed = true;
    590                }
    591
    592                out.print("  ");
    593                contextLine.prettyPrint(out);
    594                System.out.println();
    595            }
    596
    597            if (headerDisplayed) {
    598                System.out.println("(brokenObj* refers to the object for"
    599                                   + " which the invariant is broken.)");
    600                System.out.println();
    601            }
    602        }
    603
    604
    605        /** Prune out s-expressions from the counterexample context that are
    606            almost certainly irrelevant. **/
    607        //@ requires cc != null;
    608        //@ ensures \result != null;
    609        private static SList pruneCC(SList cc) throws SExpTypeError {
    610            SList copy = SList.make();
    611            SExp cur;
    612            String curS;
    613            int n = cc.length();
    614            for (int i = 0; i < n; i++) {
    615                cur = cc.at(i);
    616                curS = cur.toString();
    617                if (!cur.isList())
    618                    continue;
    619                // get rid of s-expressions that either tell you the type
    620                // of a variable or that one type subtypes another
    621                if ((curS.startsWith("(is ") || curS.startsWith("(<: ")) &&
    622                    (curS.indexOf("|T_") != -1))
    623                    continue;
    624                if(curS.indexOf("(store ") != -1 ||
    625                   curS.indexOf("(classDown ") != -1 ||
    626                   curS.indexOf("(asChild ") != -1 ||
    627                   curS.indexOf("(asLockSet ") != -1 ||
    628                   curS.indexOf("(asField ") != -1 ||
    629                   curS.indexOf("(asElems ") != -1 ||
    630                   curS.startsWith("(isAllocated ") ||
    631                   curS.startsWith("(DISTINCT "))
    632                    continue;
    633
    634                copy = copy.addEnd(cur);
    635            }
    636            return copy;
    637        }
    638
    639
    640        /********** Houdini Support ***********/
    641
    642        /**
    643         * return the string rep of the location loc when it is used
    644         * as an associated decl location.  fileNames is the CorrelatedReader
    645         * file mappings.
    646         */
    647        private static String declToFileLocStr(String loc, String fileNames[]) {
    648            int p = loc.indexOf(".");
    649            String fNum = loc.substring(0, p);
    650            int file = Integer.parseInt(fNum);
    651            loc = loc.substring(p+1);
    652
    653            p = loc.indexOf(".");
    654            String line = loc.substring(0,p);
    655            loc = loc.substring(p+1);
    656
    657            //      return fileNames[file] + ":"+line;
    658            //      return "\"" + fileNames[file] + "\"" + ":"+loc;
    659            return fileNames[file] + " " + line + " " + loc;
    660        }
    661
    662        /**
    663         * return the string rep of the location loc when it is used
    664         * as a use.  fileNames is the CorrelatedReader
    665         * file mappings.
    666         */
    667        private static String useToFileLocStr(String loc, String fileNames[]) {
    668            int p = loc.indexOf(".");
    669            String fNum = loc.substring(0, p);
    670            int file = Integer.parseInt(fNum);
    671            loc = loc.substring(p+1);
    672            p = loc.indexOf(".");
    673            return fileNames[file] + ":"+loc.substring(0,p);
    674        }
    675
    676        /**
    677         * Prints a houdini error message to out.
    678         */
    679        public static void houdiniPrint(String label,
    680                                 /*@ non_null */ PrintStream out,
    681                                 String fileNames[]) {
    682            try {
    683                if (isErrorLabel(label)) {
    684                    houdiniPrintErrorMessage(label, out, fileNames);
    685                }
    686            } catch (escjava.prover.SExpTypeError s) {
    687                Assert.fail("unexpected S-expression exception");
    688            }
    689        }
    690
    691        /** Parses <code>s</code> and prints an error message for the
    692         ** houdini log to out.
    693         **/
    694        private static void houdiniPrintErrorMessage(String s,
    695                                              /*@ non_null */ PrintStream out,
    696                                              String map[])
    697            throws SExpTypeError {
    698
    699
    700            int k = s.indexOf('@');
    701            Assert.notFalse(k != -1);
    702            String locUse = useToFileLocStr(s.substring(k+1), map);
    703            s = s.substring(0, k);
    704
    705            k = s.indexOf(':');
    706            String strLocDecl = null;
    707            if (k != -1) {
    708                strLocDecl = declToFileLocStr(s.substring(k+1), map);
    709                s = s.substring(0, k);
    710            }
    711
    712            k = s.indexOf('/');
    713            if (k != -1) {
    714                s = s.substring(0, k);
    715            }
    716
    717            int tag = TagConstants.checkFromString(s);
    718            String msg = "Warning: " + chkToMsg( tag, strLocDecl != null );
    719            out.println(strLocDecl + " " + locUse + ": " + msg);
    720        }
    721
    722
    723
    724    }