[BUG] invalid messages from static checker

Question

Following code produce five "message : CodeContracts: Suggested assumption: Assumption can be proven: Consider changing it into an assert." messages. Static checker options: Infer Ensures+Redundant Assumptions

using System.Collections.Generic;
using System.Diagnostics.Contracts;

public class Bug
{
    void F1()
    {
        F2(new List<object>());
    }

    void F2(List<object> list)
    {
        Contract.Requires(list != null);

        foreach (var item in list)
        {
            Contract.Assume(item != null);
        }
    }
}

Answer 1

That looks legit ... F2 is private and only invoked from F1, and that code path always supplies an empty list (hence no element is null).  What happens if you make F2 public?

Answer 2

Thank you for reporting it. The checker was proving some propagated postconditions (which at call site it sees as assumes).

now it is (internally) fixed.

ciao

f