#52 fix non-const old-of expressions

[Lorenzo Caminiti]

It is possible to pass non-constant expressions to CONTRACT_OLDOF therefore breaking the contract constant-correctness requirement:

int x = 0;

CONTRACT_FUNCTION(
    void (inc) ( void )
        postcondition(
            auto old_x = CONTRACT_OLDOF x = 0, // Dosen't error
            const( x, old_x ) x == old_x + 1
        )
) ;

CONTRACT_OLDOF x = 0 should error at compile-time but it does not! I can allow constant-expressions within old-of to fix this:

auto old_x = CONTRACT_OLDOF const( x ) x = 0, // Now error

The result type of the local function used to implement the constant-expression is the old-of declaration type (auto or actual type).

I also need to change the docs and Grammar to reflect this.

[Lorenzo Caminiti]

• priority changed from minor to major
• status changed from new to accepted

This is the only point in the contract where constant-correctness cannot be enforced by programmers (and it's just because I didn't notice this issue until later in the 0.4.0 release so I had no time to fix it). It should be relatively easy to support CONTRCT_ODLOF const( ... ) oldof-expr.

[Lorenzo Caminiti]

The docs should then be updated to mentioned that const can be used with CONTRACT_OLDOF (also in the Grammar section).

[Lorenzo Caminiti]

• milestone changed from Future to 1.1.0