Static checker does not find that (a+b) != (a+b+1)

[GSPP]

    static int Sum(int a, int b)
    {
        Contract.Ensures(Contract.Result<int>() == a + b);
        return a + b + 1;
    }

Should this not warn? This indeed fails at runtime with a CC exception. For example:

    static void Main()
    {
        Sum(1, 2);
    }

I configured the static checker aggressively and so far it has found other problems already so it's basically working. I also waited for cccheck.exe to exit.

I understand that the static checker is not omniscient but this seems to be a rather simple case.

Here it also does not find any problem:

    static int Sum(int a, int b)
    {
        Contract.Ensures(Contract.Result<int>() == a + b);
        return 0;
    }

Only calls to Sum are marked as errors. But it's not the call that is at fault. It's Sum. The message is:

This does not make sense to me. There is no such precondition.

---

[yaakov-h]

What happens if you disable "Infer requires"?

[GSPP]

If I turn off "Infer requires" the ensures is proven false as desired. But what possible requires could lead to the ensures not being false? It's false for all inputs. Was the requires inferred as false? :)

[yaakov-h]

No idea, I don't use Infer Requires. Suggest Requires seems to be more valuable.

If you run with Suggest Requires, does it tell you what it inferred, or does it just stay silent?

[GSPP]

Nothing is suggested in that case. Appears to be an inference bug then.

For now I'm not using the infer options per your suggestion.