Ensures on ValueType property

Question

Hello,

I have a question regarding defining ensures on simple ValueType properties. (CC v. 1.4.50327.0)

private DateTime date = DateTime.MinValue;
public DateTime Date{
  get{
    Contract.Ensures(Contract.Result<DateTime>() == this.date);
    Contract.Ensures(Contract.Result<DateTime>() == Contract.ValueAtReturn(out this.date));
    Contract.Ensures(Contract.Result<DateTime>() == Contract.OldValue(this.date));
    Contract.Ensures(Contract.Result<DateTime>().Equals(this.date));
    Contract.Ensures(DateTime.Equals(Contract.Result<DateTime>(), this.date));
    Contract.Ensures(object.Equals(Contract.Result<DateTime>(), this.date));
    return date;
  }
}

In this example only ValueAtReturn version of Ensures can be proven by static checker. When DateTime is changed to some built-in value type as Int32 there are no warnings. 

Is this the only way I can validate non-build-in value type return values or there are some plans to make other ways of varification available too?

Best Regards,

  Baal