1
Vote

Soundness bug: termination checking on delayed _(def) definitions

description

The following goes through, and therefore causes a trivially false axiom to be sent to Z3.
Having two declarations seem to be necessary to trigger the bug.

include <vcc.h>

_(abstract \natural toto()
_(decreases 0)
_(ensures 2 <= \result))

_(abstract \natural titi()
_(decreases 0)
_(ensures \result == toto() + toto()))

_(def \natural toto() { return 16; })
_(def \natural titi() { return titi() + toto(); })

comments

fdupress wrote Aug 1, 2012 at 10:52 AM

To illustrate the bug in a more compelling way, consider the following definition, that verifies when appended to the code shown above.

_(def void tata() _(ensures \false) { return; })

Sign in to add a comment or to set email notifications