search

microsoft / CodeContracts

Source code for the CodeContracts tools for .NET
Other
881 stars 150 forks source link

Warnings/messages in vs2015 #264

Open smad2005 opened 8 years ago

smad2005 commented 8 years ago

I'm using version (1.9.10714.2) from https://visualstudiogallery.msdn.microsoft.com/1ec7db13-3363-46c9-851f-1ce455f66970

Comparing to vs2013 on same project:

vs2015

the code:

using System;
using System.Collections.Generic;
using System.Text;

using System.Diagnostics.Contracts;

namespace MyContractTest
{
    class Program
    {
        private int amount;
        void TakeBottles(int i)
        {
            amount += i;
        }

        int Payday()
        {
            int today = amount;
            amount = 0;
            return today;
        }
        static void Main(string[] args)
        {
            string m = null;
            Writeline(m);
            Program r = new Program();
            r.TakeBottles(5);
            r.TakeBottles(5);
            r.TakeBottles(-20);
            Writeline(r.Payday().ToString());

        }

        [ContractInvariantMethod]
        void InvariantTest()
        {
            Contract.Invariant(amount >= 0);
        }

        static void Writeline(string s)
        {
            Contract.Requires(s != null);
            Console.WriteLine(s);
        }
    }
}
SergeyTeplyakov commented 8 years ago

Thanks for the great bug report.

Issue with error list is well known and would be fixed during next release.

Just to clarify the scope of this issue, could you please provide an outputs for both VS2013 and VS2015 (from output window)? This will help right now to understand the scope of this issue (as I said, one issue is well-known).

smad2005 commented 8 years ago

could you please provide an outputs for both VS2013 and VS2015 (from output window)?

I provided it in topic (left side (vs 2013), right side (vs2015))

the result is different in output window ( diff https://www.diffchecker.com/uxk7mw6f )

But i can provide it again

vs 2015:

1>------ Build started: Project: MyContactTest, Configuration: Debug Any CPU ------
CodeContracts: MyContactTest: Schedule static contract analysis.
1>  elapsed time: 914,7664ms
1>  MyContactTest -> C:\Downloads\hlam\MyContactTest\MyContactTest\bin\Debug\MyContactTest.exe
CodeContracts: MyContactTest: Background contract analysis started.
========== Build: 1 succeeded, 0 failed, 0 up-to-date, 0 skipped ==========
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(14,13): message : CodeContracts: Suggested requires: Contract.Requires((this.amount + i) >= 0);
CodeContracts: MyContactTest: Validated:  42,9%
CodeContracts: MyContactTest: Checked 21 assertions: 9 correct 2 unknown 9 unreached 1 false
CodeContracts: MyContactTest: Contract density: 4,09
CodeContracts: MyContactTest: Total methods analyzed 6
CodeContracts: MyContactTest: Methods analyzed with a faster abstract domain 0
CodeContracts: MyContactTest: Methods with 0 warnings 4
CodeContracts: MyContactTest: Time spent in internal, potentially costly, operations
CodeContracts: MyContactTest: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0149498 (invoked 370 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0139872 (invoked 773 times)
Overall time spent performing action #WP: 00:00:00.0670051 (invoked 2 times)
Overall time spent performing action #Simplex: 00:00:00.0670017 (invoked 7 times)
CodeContracts: MyContactTest: Total time 5,381sec. 896ms/method
CodeContracts: MyContactTest: Methods with necessary preconditions: 2
CodeContracts: MyContactTest: Discovered 2 new candidate preconditions in 00:00:00.1663306
CodeContracts: MyContactTest: Retained 2 preconditions after filtering
CodeContracts: MyContactTest: Inferred 0 object invariants
CodeContracts: MyContactTest: Retained 0 object invariants after filtering
CodeContracts: MyContactTest: Discovered 10 postconditions to suggest
CodeContracts: MyContactTest: Retained 0 postconditions after filtering
CodeContracts: MyContactTest: Detected 0 code fixes
CodeContracts: MyContactTest: Proof obligations with a code fix: 0
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(25,13): warning : CodeContracts: Invoking method 'Main' will always lead to an error. If this is wanted, consider adding Contract.Requires(false) to document it
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(25,13): warning : CodeContracts: requires is false: s != null
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(43,13): warning :   + location related to previous warning
C:\Downloads\hlam\MyContactTest\MyContactTest.exe(1,1): message : CodeContracts: Checked 21 assertions: 9 correct 2 unknown 9 unreached 1 false
CodeContracts: MyContactTest: 
CodeContracts: MyContactTest: Background contract analysis done.

vs 2013:

1>------ Build started: Project: MyContactTest, Configuration: Debug Any CPU ------
CodeContracts: MyContactTest: Schedule static contract analysis.
CodeContracts: MyContactTest: Background contract analysis started.
1>  elapsed time: 831,0496ms
1>  MyContactTest -> C:\Downloads\hlam\MyContactTest\MyContactTest\bin\Debug\MyContactTest.exe
========== Build: 1 succeeded, 0 failed, 0 up-to-date, 0 skipped ==========
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(14,13): message : CodeContracts: Suggested requires: Contract.Requires((this.amount + i) >= 0);
CodeContracts: MyContactTest: Validated:  75,0%
CodeContracts: MyContactTest: Checked 12 assertions: 9 correct 2 unknown 1 false
CodeContracts: MyContactTest: Contract density: 3,73
CodeContracts: MyContactTest: Total methods analyzed 6
CodeContracts: MyContactTest: Methods analyzed with a faster abstract domain 0
CodeContracts: MyContactTest: Methods with 0 warnings 4
CodeContracts: MyContactTest: Time spent in internal, potentially costly, operations
CodeContracts: MyContactTest: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0080315 (invoked 359 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0100056 (invoked 797 times)
Overall time spent performing action #WP: 00:00:00.0690585 (invoked 2 times)
Overall time spent performing action #Simplex: 00:00:00.0550044 (invoked 7 times)
CodeContracts: MyContactTest: Total time 4,741sec. 790ms/method
CodeContracts: MyContactTest: Methods with necessary preconditions: 2
CodeContracts: MyContactTest: Discovered 2 new candidate preconditions in 00:00:00.1706197
CodeContracts: MyContactTest: Retained 2 preconditions after filtering
CodeContracts: MyContactTest: Inferred 0 object invariants
CodeContracts: MyContactTest: Retained 0 object invariants after filtering
CodeContracts: MyContactTest: Discovered 10 postconditions to suggest
CodeContracts: MyContactTest: Retained 0 postconditions after filtering
CodeContracts: MyContactTest: Detected 0 code fixes
CodeContracts: MyContactTest: Proof obligations with a code fix: 0
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(25,13): warning : CodeContracts: Invoking method 'Main' will always lead to an error. If this is wanted, consider adding Contract.Requires(false) to document it
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(26,13): warning : CodeContracts: requires is false: s != null
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(43,13): warning :   + location related to previous warning
C:\Program Files (x86)\Microsoft Visual Studio 12.0\Common7\IDE\MyContactTest.exe(1,1): message : CodeContracts: Checked 12 assertions: 9 correct 2 unknown 1 false
CodeContracts: MyContactTest: 
CodeContracts: MyContactTest: Background contract analysis done.

Diffrence here:

vs2015 vs 2013
CodeContracts: MyContactTest: Validated: 42,9% CodeContracts: MyContactTest: Validated: 75,0%
CodeContracts: MyContactTest: Checked 21 assertions: 9 correct 2 unknown 9 unreached 1 false CodeContracts: MyContactTest: Checked 12 assertions: 9 correct 2 unknown 1 false
CodeContracts: MyContactTest: Contract density: 4,09 CodeContracts: MyContactTest: Contract density: 3,73
C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(25,13): warning : CodeContracts: requires is false: s != null C:\Downloads\hlam\MyContactTest\MyContactTest\Program.cs(26,13): warning : CodeContracts: requires is false: s != null