diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 7 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 10 | ||||
| -rw-r--r-- | Source/Core/Scanner.cs | 12 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 |
4 files changed, 20 insertions, 11 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 98086cf0..a5c63243 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -368,6 +368,7 @@ namespace Microsoft.Boogie { public bool VerifySeparately;
public string PrintFile = null;
public int PrintUnstructured = 0;
+ public bool UseBaseNameForFileName = false;
public int DoomStrategy = -1;
public bool DoomRestartTP = false;
public bool PrintDesugarings = false;
@@ -1404,7 +1405,8 @@ namespace Microsoft.Boogie { ps.CheckBooleanFlag("verifySeparately", ref VerifySeparately) ||
ps.CheckBooleanFlag("trustAtomicityTypes", ref TrustAtomicityTypes) ||
ps.CheckBooleanFlag("trustNonInterference", ref TrustNonInterference) ||
- ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false)
+ ps.CheckBooleanFlag("doNotUseParallelism", ref UseParallelism, false) ||
+ ps.CheckBooleanFlag("useBaseNameForFileName", ref UseBaseNameForFileName)
) {
// one of the boolean flags matched
return true;
@@ -1666,6 +1668,9 @@ namespace Microsoft.Boogie { Graphviz format to files named:
<prefix>.<procedure name>.dot
+ /useBaseNameForFileName : When parsing use basename of file for tokens instead
+ of the path supplied on the command line
+
---- Inference options -----------------------------------------------------
/infer:<flags>
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 8049c220..2149e12c 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -49,7 +49,7 @@ readonly StructuredCmd/*!*/ dummyStructuredCmd; ///Returns the number of parsing errors encountered. If 0, "program" returns as
///the parsed program.
///</summary>
-public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
+public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> defines, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(cce.NonNullElements(defines,true));
@@ -59,25 +59,25 @@ public static int Parse (string/*!*/ filename, /*maybe null*/ List<string/*!*/> if (filename == "stdin.bpl") {
var s = ParserHelper.Fill(Console.In, defines);
- return Parse(s, filename, out program);
+ return Parse(s, filename, out program, useBaseName);
} else {
FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
var s = ParserHelper.Fill(stream, defines);
- var ret = Parse(s, filename, out program);
+ var ret = Parse(s, filename, out program, useBaseName);
stream.Close();
return ret;
}
}
-public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program) /* throws System.IO.IOException */ {
+public static int Parse (string s, string/*!*/ filename, out /*maybe null*/ Program program, bool useBaseName=false) /* throws System.IO.IOException */ {
Contract.Requires(s != null);
Contract.Requires(filename != null);
byte[]/*!*/ buffer = cce.NonNull(UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Errors errors = new Errors();
- Scanner scanner = new Scanner(ms, errors, filename);
+ Scanner scanner = new Scanner(ms, errors, filename, useBaseName);
Parser parser = new Parser(scanner, errors, false);
parser.Parse();
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index f0c9063d..b050fcdd 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -296,7 +296,7 @@ public class Scanner { }
// [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler, bool useBaseName) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -305,7 +305,7 @@ public class Scanner { try {
Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
- Filename = fileName;
+ Filename = useBaseName? GetBaseName(fileName): fileName;
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
@@ -313,7 +313,7 @@ public class Scanner { }
// [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName, bool useBaseName) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -321,10 +321,14 @@ public class Scanner { t = new Token(); // dummy because t is a non-null field
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
- this.Filename = fileName;
+ this.Filename = useBaseName? GetBaseName(fileName) : fileName;
Init();
}
+ private string GetBaseName(string fileName) {
+ return System.IO.Path.GetFileName(fileName); // Return basename
+ }
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 92d9f898..41cfce99 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -595,7 +595,7 @@ namespace Microsoft.Boogie try
{
var defines = new List<string>() { "FILE_" + fileId };
- errorCount = Parser.Parse(bplFileName, defines, out programSnippet);
+ 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);
|