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