This project is read-only.

Re-checking memmove: Loop body invariant failed to verify

Feb 16, 2013 at 8:32 PM
Edited Feb 16, 2013 at 9:35 PM
Hi all,

I am revisiting some code from 2011 that is part of a project to add VCC annotations to standard C library functions.

I am having the problem that VCC is no longer able to verify the memmove implementation:
/* Based on code by David MacKenzie <djm@gnu.ai.mit.edu> in the Public Domain
   See: gettext-0.14.6/gettext-tools/lib/memmove.c in ftp://ftp.gnu.org/gnu/gettext/gettext-0.14.6.tar.gz */
void * memmove(void *dv, const void *sv, size_t n)
{
    size_t i;
    char *d = (char *)dv;
    const char *s = (const char *)sv;

    if (s < d)
    {
        /* Moving from low mem to hi mem; start at end. */
        for (i = n; i > 0; --i)
            _(invariant n >= i && i >= 0)
            _(invariant \forall size_t j; n >= j && j > i ==> d[j - 1] == \old(s[j - 1]))
            _(invariant \forall size_t j; i >= j && j > 0 ==> \unchanged(s[j - 1]))
        {
            _(assert n >= i && i > 0)
            _(assert n > (i - 1) && (i - 1) >= 0)
            d[i - 1] = s[i - 1];
        }

        _(assert \forall size_t j; {\match_ulong(j)} n > (j - 1) && (j - 1) >= 0 ==> d[j - 1] == \old(s[j - 1]))
        _(assert \forall size_t k; {:hint \match_ulong(k + 1)} n > k && k >= 0 ==> d[k] == \old(s[k]))
    }
    else if (s != d)
    {
        _(assert d < s)

        /* Moving from hi mem to low mem; start at beginning. */
        for (i = 0; i < n; ++i)
            _(invariant \forall size_t j; j < i ==> d[j] == \old(s[j]))
            _(invariant \forall size_t j; i <= j && j < n ==> \unchanged(s[j]))
        {
            d[i] = s[i];
        }
    }

    return dv;
}
VCC cannot verify the two "unchanged" invariants _(invariant \forall size_t j; i >= j && j > 0 ==> \unchanged(s[j - 1])) and _(invariant \forall size_t j; i <= j && j < n ==> \unchanged(s[j])).

Can someone provide some tips for getting these invariants to verify?

I am using Vcc Version 2.3.10214.0.