Skip to content

Fix file path issues in the regression test under Visual Studio 2015. #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mattmccutchen-microsoft wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Fix file path issues in the regression test under Visual Studio 2015. #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 11 additions & 16 deletions BytecodeTranslator/Program.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@
using BytecodeTranslator.TranslationPlugins;
using BytecodeTranslator.TranslationPlugins.BytecodeTranslator;
using BytecodeTranslator.TranslationPlugins.PhoneTranslator;
using System.Text;

namespace BytecodeTranslator {

Expand Down Expand Up @@ -261,25 +262,19 @@ public static int Inline(string bplFileName) {
return 0;
}

public static int TranslateAssemblyAndWriteOutput(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
public static string TranslateAssemblyAndReturnOutput(List<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> 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<string> assemblyNames, HeapFactory heapFactory, Options options, List<Regex> exemptionList, bool whiteList) {
Expand Down
44 changes: 19 additions & 25 deletions RegressionTests/TranslationTest/UnitTest0.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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<string> { assemblyName }, heapFactory, options, null, false);
var fileName = Path.ChangeExtension(assemblyName, "bpl");
var s = File.ReadAllText(fileName);
return s;
return BCT.TranslateAssemblyAndReturnOutput(new List<string> { 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());
}

}
Expand Down