1
Vote

bad unsoundness in block contracts

description

The following verifies:

void test()
_(ensures 0)
{
_(ensures 0)
{
}
}

comments

MichalMoskal wrote Jul 31, 2012 at 12:01 AM

We actually crash on this one (vcc says "confused, will now die"). The problem is the block with empty body.

This crash may not be visible in VS.

Sign in to add a comment or to set email notifications