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

Preconditions with non-interger decimals are broken #506

Open
grayed opened this issue Nov 30, 2019 · 0 comments
Open

Preconditions with non-interger decimals are broken #506

grayed opened this issue Nov 30, 2019 · 0 comments

Comments

@grayed
Copy link

grayed commented Nov 30, 2019

Here's an example. I've put a lot of Requires() to demonstrate that the issue is somehow related with decimal having fractional part, and also with placement in argument list.

using System;
using System.Diagnostics.Contracts;

namespace FodyTest
{
    class Worker
    {
        public static decimal CalcSmth(decimal foo, decimal bar, decimal buz, decimal qwe)
        {
            Contract.Requires(foo > bar);
            Contract.Requires(foo > buz);
            Contract.Requires(foo < qwe);
            Contract.Requires(bar < foo);
            Contract.Requires(bar < buz);
            Contract.Requires(bar < qwe);
            Contract.Requires(buz < foo);
            Contract.Requires(buz > bar);
            Contract.Requires(buz < qwe);
            Contract.Requires(qwe > foo);
            Contract.Requires(qwe > bar);
            Contract.Requires(qwe > buz);
            return (foo + bar + buz + qwe) / 2;
        }
    }

    class Program
    {
        static void Main(string[] args)
        {
            Console.WriteLine($"Worker.CalcSmth() returned {Worker.CalcSmth(12.0M, 1.5M, 2, 35.1M)}");
        }
    }
}

As you can see, no contracts are actually broken, but cccheck doesn't agree:

1>  CodeContracts: Task manager is unavailable (unable to run in background).
1>  CodeContracts: FodyTest: Run static contract analysis.
1>  CodeContracts: FodyTest: Time spent connecting to the cache: 00:00:03.5008095
1>  CodeContracts: FodyTest: Cache used: (LocalDb)\v11.0
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: Suggested requires: This precondition is redundant: Consider removing it
1>  CodeContracts: FodyTest: Validated: 77.8 %
1>  CodeContracts: FodyTest: Checked 18 assertions: 14 correct 4 unknown
1>  CodeContracts: FodyTest: Contract density: 2.68
1>  CodeContracts: FodyTest: Total methods analyzed 4
1>  CodeContracts: FodyTest: Methods analyzed with a faster abstract domain 0
1>  CodeContracts: FodyTest: Method analyses read from the cache 4
1>  CodeContracts: FodyTest: Methods not found in the cache 0
1>  CodeContracts: FodyTest: Methods with 0 warnings 3
1>  CodeContracts: FodyTest: Total time 1.981sec. 495ms/method
1>  CodeContracts: FodyTest: Retained 0 preconditions after filtering
1>  CodeContracts: FodyTest: Inferred 0 object invariants
1>  CodeContracts: FodyTest: Retained 0 object invariants after filtering
1>  CodeContracts: FodyTest: Detected 0 code fixes
1>  CodeContracts: FodyTest: Proof obligations with a code fix: 0
1>C:\Users\user\source\repos\FodyTest\Program.cs(30,13,30,103): warning : CodeContracts: requires unproven: foo > bar
1>C:\Users\user\source\repos\FodyTest\Program.cs(10,13,10,42): warning : CodeContracts: location related to previous warning
1>C:\Users\user\source\repos\FodyTest\Program.cs(30,13,30,103): warning : CodeContracts: requires unproven: foo > buz
1>C:\Users\user\source\repos\FodyTest\Program.cs(11,13,11,42): warning : CodeContracts: location related to previous warning
1>C:\Users\user\source\repos\FodyTest\Program.cs(30,13,30,103): warning : CodeContracts: requires unproven: foo < qwe
1>C:\Users\user\source\repos\FodyTest\Program.cs(12,13,12,42): warning : CodeContracts: location related to previous warning
1>C:\Users\user\source\repos\FodyTest\Program.cs(30,13,30,103): warning : CodeContracts: requires unproven: bar < buz
1>C:\Users\user\source\repos\FodyTest\Program.cs(14,13,14,42): warning : CodeContracts: location related to previous warning
1>  CodeContracts: Checked 18 assertions: 14 correct 4 unknown
1>  CodeContracts: FodyTest: 
1>  CodeContracts: FodyTest: Static contract analysis done.
========== Build: 1 succeeded, 0 failed, 0 up-to-date, 0 skipped ==========

Visual Studio 2019 16.3.10
.NET Framework 4.8.03752
Installed NuGet packages System.Diagnostic.Contracts 4.3.0 and CodeContracts.MSBuild.v2 1.13.0.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant