[boost] [contract] Broken postconditions on throw

Subject: [boost] [contract] Broken postconditions on throw
From: Andrzej Krzemienski (akrzemi1_at_[hidden])
Date: 2012-08-26 15:10:25

Hi Lorenzo,
I am now now playing with Contract library and trying to break it. I
checked that the framework checks the class invariant even when member
function exits via an exception. This is an expected behavior and the
framework is working fine. However, I note that the precondition of a
(non-member) function is not checked when the function exits via throwing
an exception. See the following program:

# include <contract.hpp>

double get_random_weight()
{
    return -1.0; // erroneous implementation
}

CONTRACT_FUNCTION (
    void (set_weight)( (double&) w )
    postcondition(w >= 0.0)
)
{
    w = get_random_weight();
    if (w < 0.0) throw 1; // (*)
}

int main() try {
    double w = 0.0;
    set_weight(w);
}
catch (...) {
    std::cerr << "CAUGHT EXCEPTION" << std::endl;
}

Function set_weight() is intended to assign its (output) argument with a
value representing weight (in the physical sense). We guarantee that the
value we set is always non-negative. The function clumsily attempts to
verify the condition itself (the line with *). It signals the failure with
an exception, but unfortunately fails to satisfy the postcondition. I
expect that this situation should be reported as a postcondition violation.
But no violation is reported, and the program successfully outputs "CAUGHT
EXCEPTION".

Regards,
&rzej