CODEWITHSUNDEEP
molespex
Boymix81
Boymix81

Reputation: 31

Pex suggest a solution with Moles's error

I try to use Pex to explore the following method :

public float MultiplyFloat(float a, float j)
{
    if (a * a == 2)
    {
    if (j == 123)
    {
        a = 2;
    }
    }
    else
    a = 3;

    return 3;
}

I know that the Z3 is a linear arithmetic solver and floating point is not supported but Pex wizard in Visual Studio 2010 add-on suggest me to "Moles Type" , I use this suggest and Pex Wizard create :

1) the Microsoft.Pex.Framework.moles file

<Moles xmlns="http://schemas.microsoft.com/moles/2010/">
  <Assembly Name="Microsoft.Pex.Framework" />
</Moles>

2) a prepared class : __TestabilityHelperPreparation

using System;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Engine.Symbols.Moles;
using Microsoft.Pex.Engine.Symbols;

namespace Microsoft.Pex.Engine.Symbols.Preparations
{
    /// <summary>Contains a method to prepare the type __TestabilityHelper</summary>
    public static partial class __TestabilityHelperPreparation
    {
        /// <summary>Prepares the environment (and the moles) before executing any method of the prepared type __TestabilityHelper</summary>
        [PexPreparationMethod(typeof(__TestabilityHelper))]
        public static void Prepare()
        {
            M__TestabilityHelper.BehaveAsCurrent();
            // TODO: use Moles to replace API that call into the environment
        }
    }
}

but not compile with the following errors :

C:\Program Files (x86)\Microsoft\Contracts\MsBuild\v4.0\Microsoft.CodeContracts.targets(274,5): error MSB3073: uscita dal comando ""C:\Program Files (x86)\Microsoft SDKs\Windows\v8.0A\Bin\sn.exe" /R "o\Microsoft.Pex.Framework.Moles.dll" "m.g.snk"" con codice 9009. [D:\BenchMarkTesterToolLib.Tests02\obj\Debug\Moles\mpf\m.g.csproj]

Moles compilation FAILED - 58,028916314783s

C:\Program Files\Microsoft Moles\bin\Microsoft.Moles.targets(79,5): error MSB3073: uscita dal comando ""C:\Program Files\Microsoft Moles\bin\moles.exe" @D:\BenchMarkTesterToolLib.Tests02\obj\Debug\Moles\moles.args" con codice -1002.

So, Do I an error or is Pex to suggest me a wrong solution ?

Thanks.

Upvotes: 1

Views: 205

Answers (1)

Bob Vale
Bob Vale

Reputation: 18474

The problem is actually with Code Contracts, it is running the wrong version of sn. This has been fixed in the latest version of Code Contracts. So try updating Code Contracts and try again.

Upvotes: 1

Related Questions