summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine
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 /Source/ExecutionEngine
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.
Diffstat (limited to 'Source/ExecutionEngine')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs2
1 files changed, 1 insertions, 1 deletions
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);