summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-04-06 16:47:11 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-04-06 16:47:11 +0100
commit71f8c1bb366154083ff5eff5943520d9511ea014 (patch)
tree8fd06d4dad5b36011db3ae7aa19d9fa0f4838c85
parent0a1ced90f52b5572d0ffef0a476a1bb4270522c2 (diff)
Added /useBaseNameForFile command line argument. The Scanner
and Parser constructors have been modified to take an optional argument specifying this and the ExecutionEngine passes for that value CommandLineOptions.Clo.UseBaseNameForFileName This option when true causes the basename of file to be used inside created Tokens instead of what the user passed on the command line which might be a relative or absolute path. The motivation for adding this option is that it is needed for the lit driven tests so that the output of Boogie can be reliably checked.
-rw-r--r--Source/Core/CommandLineOptions.cs7
-rw-r--r--Source/Core/Parser.cs10
-rw-r--r--Source/Core/Scanner.cs12
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs2
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);