From fedb120d984e00f7aabc342e2df5c45f0dec3484 Mon Sep 17 00:00:00 2001 From: Matt McCutchen Date: Mon, 20 Jun 2016 14:02:56 -0700 Subject: [PATCH] Fix file path issues in the regression test under Visual Studio 2015. The test was looking for RegressionTestInput.dll in the test output directory without having copied it there, and it was writing the actual outputs to TranslationTest\bin\Debug instead of the test output directory. I'm not sure how this was supposed to work before, but hopefully this change does not break any other use modes. --- BytecodeTranslator/Program.cs | 27 +++++------- RegressionTests/TranslationTest/UnitTest0.cs | 44 +++++++++----------- 2 files changed, 30 insertions(+), 41 deletions(-) diff --git a/BytecodeTranslator/Program.cs b/BytecodeTranslator/Program.cs index f9a43b6..ff94543 100644 --- a/BytecodeTranslator/Program.cs +++ b/BytecodeTranslator/Program.cs @@ -24,6 +24,7 @@ using BytecodeTranslator.TranslationPlugins; using BytecodeTranslator.TranslationPlugins.BytecodeTranslator; using BytecodeTranslator.TranslationPlugins.PhoneTranslator; +using System.Text; namespace BytecodeTranslator { @@ -261,25 +262,19 @@ public static int Inline(string bplFileName) { return 0; } - public static int TranslateAssemblyAndWriteOutput(List assemblyNames, HeapFactory heapFactory, Options options, List exemptionList, bool whiteList) { + public static string TranslateAssemblyAndReturnOutput(List assemblyNames, HeapFactory heapFactory, Options options, List exemptionList, bool whiteList) { Contract.Requires(assemblyNames != null); Contract.Requires(heapFactory != null); - try { - var pgm = TranslateAssembly(assemblyNames, heapFactory, options, exemptionList, whiteList); - var fileName = assemblyNames[0]; - fileName = Path.GetFileNameWithoutExtension(fileName); - string outputFileName = fileName + ".bpl"; - using (var writer = new Microsoft.Boogie.TokenTextWriter(outputFileName)) { - Prelude.Emit(writer); - pgm.Emit(writer); - writer.Close(); - } - return 0; // success - } catch (Exception e) { // swallow everything and just return an error code - Console.WriteLine("The byte-code translator failed: {0}", e.Message); - // Console.WriteLine("Stack trace: {0}", e.StackTrace); - return -1; + var pgm = TranslateAssembly(assemblyNames, heapFactory, options, exemptionList, whiteList); + var fileName = assemblyNames[0]; + fileName = Path.GetFileNameWithoutExtension(fileName); + string outputFileName = fileName + ".bpl"; + var sb = new StringBuilder(); + using (var writer = new Microsoft.Boogie.TokenTextWriter(outputFileName, new StringWriter(sb), false)) { + Prelude.Emit(writer); + pgm.Emit(writer); } + return sb.ToString(); } public static Bpl.Program/*?*/ TranslateAssembly(List assemblyNames, HeapFactory heapFactory, Options options, List exemptionList, bool whiteList) { diff --git a/RegressionTests/TranslationTest/UnitTest0.cs b/RegressionTests/TranslationTest/UnitTest0.cs index 62ce915..fcdc0b9 100644 --- a/RegressionTests/TranslationTest/UnitTest0.cs +++ b/RegressionTests/TranslationTest/UnitTest0.cs @@ -38,6 +38,9 @@ public TestContext TestContext { } } + private string InputAssemblyPath => + typeof(RegressionTestInput.Class0).Assembly.Location; + #region Additional test attributes // // You can use the following additional attributes as you write your tests: @@ -64,42 +67,33 @@ private string ExecuteTest(string assemblyName, HeapFactory heapFactory) { var options = new Options(); options.monotonicHeap = true; options.dereference = Options.Dereference.Assume; - BCT.TranslateAssemblyAndWriteOutput(new List { assemblyName }, heapFactory, options, null, false); - var fileName = Path.ChangeExtension(assemblyName, "bpl"); - var s = File.ReadAllText(fileName); - return s; + return BCT.TranslateAssemblyAndReturnOutput(new List { assemblyName }, heapFactory, options, null, false); } - [TestMethod] - public void SplitFieldsHeap() { - string dir = TestContext.DeploymentDirectory; - var fullPath = Path.Combine(dir, "RegressionTestInput.dll"); - Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.SplitFieldsHeapInput.txt"); + private void ComparisonTest(string name, Heap heap) + { + Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream( + "TranslationTest." + name + "Input.txt"); StreamReader reader = new StreamReader(resource); string expected = reader.ReadToEnd(); - var result = ExecuteTest(fullPath, new SplitFieldsHeap()); - if (result != expected) { - string resultFile = Path.GetFullPath("SplitFieldsHeapOutput.txt"); + var result = ExecuteTest(InputAssemblyPath, new SplitFieldsHeap()); + if (result != expected) + { + string resultFile = Path.Combine(TestContext.DeploymentDirectory, name + "Output.txt"); File.WriteAllText(resultFile, result); - var msg = String.Format("Output didn't match: SplitFieldsHeapInput.txt \"{0}\"", resultFile); + var msg = String.Format("Output didn't match: {0}Input.txt \"{1}\"", name, resultFile); Assert.Fail(msg); } } + [TestMethod] + public void SplitFieldsHeap() { + ComparisonTest("SplitFieldsHeap", new SplitFieldsHeap()); + } + [TestMethod] public void GeneralHeap() { - string dir = TestContext.DeploymentDirectory; - var fullPath = Path.Combine(dir, "RegressionTestInput.dll"); - Stream resource = typeof(UnitTest0).Assembly.GetManifestResourceStream("TranslationTest.GeneralHeapInput.txt"); - StreamReader reader = new StreamReader(resource); - string expected = reader.ReadToEnd(); - var result = ExecuteTest(fullPath, new GeneralHeap()); - if (result != expected) { - string resultFile = Path.GetFullPath("GeneralHeapOutput.txt"); - File.WriteAllText(resultFile, result); - var msg = String.Format("Output didn't match: GeneralHeapInput.txt \"{0}\"", resultFile); - Assert.Fail(msg); - } + ComparisonTest("GeneralHeap", new GeneralHeap()); } }