From d19da5e5ec8259f6b49ec4c3c6b28bf5c25e8f15 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 9 Apr 2014 21:58:08 +0100
Subject: Teach the ExecutionEngine to respect the -useBaseNameForFileName
 commandline option when reporting the number of errors.

---
 Source/ExecutionEngine/ExecutionEngine.cs | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 41cfce99..acb329ed 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -586,7 +586,7 @@ namespace Microsoft.Boogie
           }
           if (CommandLineOptions.Clo.Trace)
           {
-            Console.WriteLine("Parsing " + bplFileName);
+            Console.WriteLine("Parsing " + GetFileNameForConsole(bplFileName));
           }
         }
 
@@ -598,14 +598,14 @@ namespace Microsoft.Boogie
           errorCount = Parser.Parse(bplFileName, defines, out programSnippet, CommandLineOptions.Clo.UseBaseNameForFileName);
           if (programSnippet == null || errorCount != 0)
           {
-            Console.WriteLine("{0} parse errors detected in {1}", errorCount, bplFileName);
+            Console.WriteLine("{0} parse errors detected in {1}", errorCount, GetFileNameForConsole(bplFileName));
             okay = false;
             continue;
           }
         }
         catch (IOException e)
         {
-          printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", bplFileName, e.Message);
+          printer.ErrorWriteLine(Console.Out, "Error opening file \"{0}\": {1}", GetFileNameForConsole(bplFileName), e.Message);
           okay = false;
           continue;
         }
@@ -632,6 +632,11 @@ namespace Microsoft.Boogie
       }
     }
 
+    private static string GetFileNameForConsole(string filename)
+    {
+      return (CommandLineOptions.Clo.UseBaseNameForFileName) ? System.IO.Path.GetFileName(filename) : filename;
+    }
+
 
     /// <summary>
     /// Resolves and type checks the given Boogie program.  Any errors are reported to the
@@ -659,7 +664,7 @@ namespace Microsoft.Boogie
       int errorCount = program.Resolve();
       if (errorCount != 0)
       {
-        Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, bplFileName);
+        Console.WriteLine("{0} name resolution errors detected in {1}", errorCount, GetFileNameForConsole(bplFileName));
         return PipelineOutcome.ResolutionError;
       }
 
@@ -673,7 +678,7 @@ namespace Microsoft.Boogie
       errorCount = program.Typecheck();
       if (errorCount != 0)
       {
-        Console.WriteLine("{0} type checking errors detected in {1}", errorCount, bplFileName);
+        Console.WriteLine("{0} type checking errors detected in {1}", errorCount, GetFileNameForConsole(bplFileName));
         return PipelineOutcome.TypeCheckingError;
       }
 
@@ -686,7 +691,7 @@ namespace Microsoft.Boogie
       moverTypeChecker.TypeCheck();
       if (moverTypeChecker.errorCount != 0)
       {
-          Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, bplFileName);
+          Console.WriteLine("{0} type checking errors detected in {1}", moverTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
           return PipelineOutcome.TypeCheckingError;
       }
 
@@ -698,7 +703,7 @@ namespace Microsoft.Boogie
       }
       else
       {
-        Console.WriteLine("{0} type checking errors detected in {1}", linearTypeChecker.errorCount, bplFileName);
+        Console.WriteLine("{0} type checking errors detected in {1}", linearTypeChecker.errorCount, GetFileNameForConsole(bplFileName));
         return PipelineOutcome.TypeCheckingError;
       }
 
-- 
cgit v1.2.3