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    }