CodePlexProject Hosting for Open Source Software

VCC supports various integer models. By default all C integers are mapped to mathematical integers, i.e., arbitrary precision integers. In this mode users have to prove that there is no overflow in the program. For example, consider the
following example:

There are three ways to deal with this:

1. Strengthen the precondition to guarantee that overflow cannot occur:

2. Suppress the overflow check in the body of the succ function, and weaken the postcondition to account for the possibility of overflow:

Inserting _(unchecked) comes at a price, though: explicit annotation is usually needed to reason about the actual value of _(unchecked) (i+1). The main things that VCC knows about unchecked expressions are that (1) if e is a value within the range of its type, then _(unchecked) e == e, and (2) some facts about addition, e.g. if x and y are unsigned ints, then _(unchecked)(x+y) == (UINT_MAX - x < y) ? (y - (UINT_MAX - x)) : (x + y).

3. Finally, you can suppress underflow and overflow checking altogether by calling VCC with the /checked- flag on the original source. This option is sometimes useful when you want to concentrate on the algorithm (as opposed to its implementation), but of course it is unsound. In effect, it is assuming that operations don't underflow/overflow, and so is not a sound way to reason about algorithms designed to operate under unbounded arithmetic. If this is what you want to do, you should instead use mathematical data types like \integer and \natural (in ghost code).

#include <vcc.h> int succ(int i) _(ensures \result == i+1) { return i+1; // fails with overflow }

There are three ways to deal with this:

1. Strengthen the precondition to guarantee that overflow cannot occur:

#include <vcc.h> #include <limits.h> int succ(int i) _(requires i<INT_MAX) _(ensures \result == i+1) { return i+1; }

2. Suppress the overflow check in the body of the succ function, and weaken the postcondition to account for the possibility of overflow:

#include <vcc.h> int succ(int i) _(ensures \result == \unchecked(i+1)) { return _(unchecked) (i+1); }

Inserting _(unchecked) comes at a price, though: explicit annotation is usually needed to reason about the actual value of _(unchecked) (i+1). The main things that VCC knows about unchecked expressions are that (1) if e is a value within the range of its type, then _(unchecked) e == e, and (2) some facts about addition, e.g. if x and y are unsigned ints, then _(unchecked)(x+y) == (UINT_MAX - x < y) ? (y - (UINT_MAX - x)) : (x + y).

3. Finally, you can suppress underflow and overflow checking altogether by calling VCC with the /checked- flag on the original source. This option is sometimes useful when you want to concentrate on the algorithm (as opposed to its implementation), but of course it is unsound. In effect, it is assuming that operations don't underflow/overflow, and so is not a sound way to reason about algorithms designed to operate under unbounded arithmetic. If this is what you want to do, you should instead use mathematical data types like \integer and \natural (in ghost code).

Last edited May 2, 2012 at 9:38 PM by erniecohen, version 13