Fix regression tests (Analyze1FromSourcesV40)

[tom-englert]

Fix the Analyze1FromSourcesV40 regression tests. (for #148)

• offset changes
• changes due to fixed system contracts

Should not be pulled before #152, #153 and #154

[SergeyTeplyakov]

I'm going to merge this stuff. Any objections? @tom-englert, @sharwell

[sharwell]

Merging #152, #153, and #154 should not be a problem. After that, we will need to rebase this pull request before it can be merged.

[tom-englert]

I will rebase this as soon as the others are merged.

[SergeyTeplyakov]

I assume that the fix was rebased. If there is no objections I'll merge the PR.

[sharwell]

@SergeyTeplyakov No, this pull request is still waiting for #152, #153, and #154 to be merged.

[SergeyTeplyakov]

Merged #152, #153, and #154.

[sharwell]

👍 We'll take a look at updating this now 😄

[tom-englert]

Rebased, ready to pull 👍

[sharwell]

❗ Please revert this header change (and any like it).

Edit: This is part of the first three formatting commits which can simply be dropped from this pull request. 😄

[tom-englert]

So the two lines header is the correct one?

[sharwell]

❗ Can you rebase this to not include the first three commits?

[tom-englert]

OK, just committed the functional changes.
I thought the formatting changes would be gone after merging automatically, but somehow they survived.

[sharwell]

Changes to fix the tests look fine. I would prefer to separate the culture change to its own pull request, but I'll leave the call up to @SergeyTeplyakov. Overall 👍.

[tom-englert]

p.s. there is already an issue to make string-formatting culture-independent: #149

[panacekcz]

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).

[SergeyTeplyakov]

@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.

[tom-englert]

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