1
Vote

min/max causes nullpointer exception

description

The following code results in a Nullreference Exception when built with Visual Studio 2008.
<p>
I'm not sure whether this syntax of min and max is supported as I have seen some examples only.

file attachments

comments

borishollas wrote Aug 9, 2010 at 11:10 AM

This problem persists with Spec# 2010-07-20.

rustanleino wrote Aug 9, 2010 at 11:46 PM

This is a bug. It seems that the combination of "old" with min/max causes the compiler to crash.

Beyond that, it seems there's also a second bug, which is that the type of min/max comes out as "int", even when the operands are "long" as in this case.

As a workaround, you can write:
ensures 0   _value == (old(_value) + amount   _value == (old(_value) + amount 
    _value 
    old(_value) + amount <= _value && 0 <= _value &&
    (_value == old(_value) + amount || _value == 0);
Also, the body of the "increase" method is not correct.

Sign in to add a comment or to set email notifications