Skip to content
This repository was archived by the owner on Jul 15, 2023. It is now read-only.

Fix regression tests (Analyze1FromSourcesV40) #151

Merged
SergeyTeplyakov merged 2 commits into from
Aug 15, 2015
Merged

Fix regression tests (Analyze1FromSourcesV40) #151

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
233ff7d
Fix regression tests (Analyze1FromSourcesV40)
tom-englert Jul 18, 2015
61190f0
Some code depends on the current culture, therefore set the main thre…
tom-englert Jul 18, 2015
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
5 changes: 5 additions & 0 deletions Microsoft.Research/ClousotMain/ClousotMain.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,6 +36,7 @@
using Microsoft.Research.ClousotPulse.Messages;
using Microsoft.Research.CodeAnalysis.Inference;
using System.IO.Pipes;
using System.Globalization;

// Because these classes and methods can be called from different places (Console, Visual Studio, WCF Service, ...)
// - do not use Console unless guarded with #if DEBUG. Instead use output
Expand Down Expand Up @@ -795,6 +796,10 @@ static IOutputFullResults<Method, Assembly> SelectOutput(

public int Analyze()
{
// String formatting in the analyzer does not specify a culture, therefore some tests fail on systems with non-English culture with e.g. "expected: 2.0, actual: 2,0"
// Setting the threads culture should be removed as soon as issue #149 is fixed.
Thread.CurrentThread.CurrentCulture = CultureInfo.InvariantCulture;
Copy link
Contributor

@sharwell sharwell Aug 13, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

❗ I would be comfortable with this in the test suite, but not in the application itself. We should find another way if at all possible.

Copy link
Contributor Author

@tom-englert tom-englert Aug 13, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The other way is to fix thousands of formatting statements where the culture is missing.

Pros for this way of fixing (until all the code is culture-specific):

  • All the code has never been verified using another culture than US(~Invariant).
  • The only thing affected by this would be the UI - but the analyzer does not have one.

Copy link
Contributor

@sharwell sharwell Aug 13, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can we not put it in the test suite initialization code?

Copy link
Contributor Author

@tom-englert tom-englert Aug 13, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The tests are just calling the .exe - we would need another argument to pass the culture to the other process.

Copy link
Contributor

@sharwell sharwell Aug 13, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The tests are just calling the .exe - we would need another argument to pass the culture to the other process.

That would be preferable. My vote is for /LCID to match devenv.exe.

Copy link
Contributor

@panacekcz panacekcz Aug 14, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 What about using invariant culture if /regression option is used? Possible implementation: 4c98ec5
I think a more complicated /LCID does not add much value (why would you use it other than for this?).


try
{
return InternalAnalyze();
Expand Down
6 changes: 6 additions & 0 deletions Microsoft.Research/RegressionTest/ClousotTests/ClousotTests.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,6 +179,12 @@
<None Include="..\TestFrameworkOOB\UserFeedback.cs">
<Link>Sources\UserFeedback.cs</Link>
</None>
<Compile Include="..\IteratorAnalysis\IteratorSimpleContract\IteratorSimpleContract.cs">
<Link>Sources\IteratorSimpleContract.cs</Link>
</Compile>
<Compile Include="..\TestPostconditionInference\Filtering.cs">
<Link>Sources\Filtering.cs</Link>
Copy link
Contributor

@panacekcz panacekcz Aug 13, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This file causes ClousotTests not to show in Test Explorer, because it contains methods declared extern.

Error loading C:\…\CodeContracts\Microsoft.Research\RegressionTest\ClousotTests\bin\Debug\ClousotTests.dll: Unable to load the test container 'C:\…\CodeContracts\Microsoft.Research\RegressionTest\ClousotTests\bin\Debug\ClousotTests.dll' or one of its dependencies. Error details:
System.TypeLoadException: Could not load type 'TestPostconditionInference.FilterRedundantPostcondition' from assembly 'ClousotTests, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null' because the method 'GetApplicationVersion' has no implementation (no RVA).
System.TypeLoadException: Could not load type 'TestPostconditionInference.Array' from assembly 'ClousotTests, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null' because the method 'get_Length' has no implementation (no RVA).

Copy link
Contributor

@SergeyTeplyakov SergeyTeplyakov Aug 15, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@sharwell I prefer separate PR, but separate commits are fine for now.

@tom-englert What do you think about @panacekcz comment? We can fix this in separate commit/PR.

Copy link
Contributor Author

@tom-englert tom-englert Aug 17, 2015

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These files should have been added as <None>, not as <Compile>.
It's only to have the test files part of the project.

</Compile>
<Compile Include="Tests.cs" />
<None Include="..\Containers\TestContainers\ArrayWithNonNullAnalysis.cs">
<Link>Sources\ArrayWithNonNullAnalysis.cs</Link>
Expand Down
2 changes: 1 addition & 1 deletion Microsoft.Research/RegressionTest/ClousotTests/Sources/Abbreviators.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ public void Work3()
}

[ClousotRegressionTest]
[RegressionOutcome(Outcome = ProofOutcome.False, Message = "ensures is false: this.X == Contract.OldValue(this.X)", PrimaryILOffset = 19, MethodILOffset = 20)]
[RegressionOutcome(Outcome = ProofOutcome.False, Message = "ensures is false: X == Contract.OldValue(X)", PrimaryILOffset = 19, MethodILOffset = 20)]
[RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = @"ensures unreachable", PrimaryILOffset = 43, MethodILOffset = 20)]
[RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = @"ensures unreachable", PrimaryILOffset = 67, MethodILOffset = 20)]
public void Work4()
Expand Down
4 changes: 2 additions & 2 deletions Microsoft.Research/RegressionTest/ClousotTests/Sources/IOperations.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,8 @@ public Type[] Types
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 8, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 11, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 11, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 52, MethodILOffset = 36)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 77, MethodILOffset = 36)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 52, MethodILOffset = 31)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "ensures is valid", PrimaryILOffset = 77, MethodILOffset = 31)]
public double Do(params object[] operands)
{
Console.Write(string.Format("We have {0} {1}s\n", operands[1], operands[0]));
Expand Down
345 changes: 180 additions & 165 deletions ...Research/RegressionTest/IteratorAnalysis/IteratorSimpleContract/IteratorSimpleContract.cs
View file
Open in desktop

Large diffs are not rendered by default.

1 change: 1 addition & 0 deletions Microsoft.Research/RegressionTest/TestFrameworkOOB/Purity.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ public static void Test(object a, object b)
[ClousotRegressionTest]
[RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly calling a method on a null reference \'dict\'", PrimaryILOffset = 3, MethodILOffset = 0), RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 16, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 21, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 16)]
public static void Test(IDictionary<int, string> dict, int key)
{
Contract.Requires(dict.ContainsKey(key));
Expand Down
5 changes: 4 additions & 1 deletion Microsoft.Research/RegressionTest/TestFrameworkOOB/ReferenceToAllOOBC.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,8 @@ public static void Test2()
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 28, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 38, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 51, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 18)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 28)]
public static void TestPureLookup(Dictionary<int, string> dict, int key)
{
Contract.Requires(dict != null);
Expand All @@ -73,6 +75,8 @@ public static void TestPureLookup(Dictionary<int, string> dict, int key)
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 18, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 34, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 54, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 18)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 21, MethodILOffset = 34)]
public static void TestOutByRef()
{
var d = new Dictionary<string, object>();
Expand Down Expand Up @@ -473,7 +477,6 @@ private static void Test2(IEnumerable<string> elements)
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 100, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 141, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 154, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 166, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "Lower bound access ok", PrimaryILOffset = 60, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "Upper bound access ok", PrimaryILOffset = 60, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 15, MethodILOffset = 133)]
Expand Down
21 changes: 11 additions & 10 deletions Microsoft.Research/RegressionTest/TestFrameworkOOB/UserFeedback.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,13 +228,13 @@ internal class Some
[ClousotRegressionTest("cci2only")]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 2, MethodILOffset = 0)]
#if NETFRAMEWORK_4_0
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 33, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 57, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 72, MethodILOffset = 0)]
[RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=33,MethodILOffset=0)]
[RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=57,MethodILOffset=0)]
[RegressionOutcome(Outcome=ProofOutcome.Bottom,Message="assert unreachable",PrimaryILOffset=72,MethodILOffset=0)]
#else
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 29, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 53, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 68, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = "assert unreachable", PrimaryILOffset = 68, MethodILOffset = 0)]
#endif
public void WaitFor0()
{
Expand All @@ -259,15 +259,15 @@ public void WaitFor0()
[ClousotRegressionTest("cci2only")]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 2, MethodILOffset = 0)]
#if NETFRAMEWORK_4_0
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 33, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 50, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 62, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 77, MethodILOffset = 0)]
[RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=33,MethodILOffset=0)]
[RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=50,MethodILOffset=0)]
[RegressionOutcome(Outcome=ProofOutcome.True,Message="valid non-null reference (as field receiver)",PrimaryILOffset=62,MethodILOffset=0)]
[RegressionOutcome(Outcome=ProofOutcome.Bottom,Message="assert unreachable",PrimaryILOffset=77,MethodILOffset=0)]
#else
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 29, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 46, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as field receiver)", PrimaryILOffset = 58, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "assert is valid", PrimaryILOffset = 73, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.Bottom, Message = "assert unreachable", PrimaryILOffset = 73, MethodILOffset = 0)]
#endif
public void WaitFor0WithLockObject()
{
Expand Down Expand Up @@ -344,6 +344,7 @@ private void AddItemToDict(string key, object value)
[RegressionOutcome(Outcome = ProofOutcome.Top, Message = "Possibly calling a method on a null reference \'this._dict\'", PrimaryILOffset = 8, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "valid non-null reference (as receiver)", PrimaryILOffset = 21, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = "requires is valid", PrimaryILOffset = 16, MethodILOffset = 21)]
[RegressionOutcome(Outcome = ProofOutcome.Top, Message = "requires unproven: !ReferenceEquals(key, null)", PrimaryILOffset = 21, MethodILOffset = 8)]
private void ProcessItem(string key, object value)
{
if (!_dict.ContainsKey(key))
Expand Down Expand Up @@ -875,7 +876,7 @@ public void Baz()
[ClousotRegressionTest]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as receiver)", PrimaryILOffset = 8, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.True, Message = @"valid non-null reference (as receiver)", PrimaryILOffset = 15, MethodILOffset = 0)]
[RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: this.Prop2 != 0", PrimaryILOffset = 13, MethodILOffset = 15)]
[RegressionOutcome(Outcome = ProofOutcome.Top, Message = @"requires unproven: Prop2 != 0", PrimaryILOffset = 13, MethodILOffset = 15)]
private static void Test()
{
Foo foo = new Foo();
Expand Down
Loading