This project is read-only.

Contradictory requirements

Feb 18, 2011 at 12:53 PM

Is there any way to detect unsatisfiable preconditions.  I had thought that /smoke would do so, but it seems that it doesn't.

C:   type test.c
#include <vcc.h>

int test(int i)
_(requires i==0)
_(requires i==1)
_(ensures \result == 1)
{
        return i ;
}

C:  vcc/2/it/smoke test.c
Verification of test succeeded.


Feb 18, 2011 at 1:54 PM
Edited Feb 18, 2011 at 1:54 PM

you can always test your specifications by adding an explicit "assert(\false);" at the end of a function. if it verifies, there must be an inconsistency somewhere.

Feb 18, 2011 at 2:54 PM

There seems to be some bug in the option processing code. The missing spaces in your call cause VCC neither to do the smoke-check nor complain. If you add spaces, smoke check will catch the problem:



C:\Temp>type test.c

#include 

int test(int i)
_(requires i==0)
_(requires i==1)
_(ensures \result == 1)
{
        return i ;
}


C:\Temp>vcc/2/it/smoke test.c
Verification of test succeeded.

C:\Temp>vcc /2 /it /smoke test.c
Verification of test succeeded.
C:\Temp\test.c(7): found unreachable code, possible soundness violation, please
check the axioms or add an explicit assert(false)

Feb 19, 2011 at 12:42 PM

Thanks Mark.  That sure helps.

Cheers,

Theo