Incorrect "Suggest Ensures" scenario with array bounds

Question

I have added only two lines in a default Windows Console Application project:

static void Main(string[] args) {
  Contract.Requires(args.Length > 10);
  Console.WriteLine(args[10]);
}

When I compile this project with Code Contracts ("Perform Static Contract Checking" and "Suggest Ensures" are checked), I get a message:

…\Program.cs(13,7): message : CodeContracts: Suggested ensures: Contract.Ensures(Contract.ForAll(0, args.Length, __k__ => args[__k__] != 0));

Is this suggession are correct? How can I fix this ("args[__k__] != 0" can not be compiled, because args[__k__] is string)?

UPD: Code Contracts version is 1.4.50327.0 (March 27, 2012).

---

Viacheslav Ivanov aka _FRED_

Answer 1

sorry. the suggestion should be:

args[__k__] != null

In the IL null and 0 are the same this is why the static checker suggests the wrongly typed postcondition.

thanks

f

Answer 2

After changing my code:

static void Main(string[] args) {
  Contract.Requires(args.Length > 10);
  Contract.Ensures(Contract.ForAll(0, args.Length, index => args[index] != null));
  Console.WriteLine(args[10]);
}

I still have a suggestion: "(1,1): message : CodeContracts: Suggested ensures: Program.Main(System.String[])[0x0]: Contract.Ensures(Contract.ForAll(0, args.Length, __k__ => args[__k__] != 0));" File name does not specified in an output. Is this correct?

---

Viacheslav Ivanov aka _FRED_

Answer 3

The postcondition suggestion is only to help the annotation process.

What is happening here is that we have a special case for Main where the static checker knows that args != and all its elements are not null, as guaranteed by the environment.

As the array is not modified, the static checker reports that this condition holds also at the end of the method. This is just a suggestion, you can turn the "suggest ensures" off if it causes too much noise.

ciao

f