[CN] Cannot mark preexisting variable as not changing value in a loop

[peterohanley]

I would like the body of the inner loop to be able to rely on the c it accesses matching the c before it, as well as the c in its own invariant. This was my first attempt:

#include <stdint.h>

void
foo(void)
{
    for(int c = 0; c < 1; ++c)
    /*@ inv 0i32 <= c; c <= 1i32;
    @*/
    {
        int k = c;
        for (int i = 0; i < 1; ++i)
        /*@ inv 0i32 <= i; i <= 1i32;
            0i32 <= c; c < 1i32;
            {&k} unchanged;
            {&c} unchanged;
        @*/
        {
            /*@ assert(k==c);@*/
        }
    }
}

This works:

void
foo3(void)
{
    for(int c = 0; c < 1; ++c)
    /*@ inv 0i32 <= c; c <= 1i32;
    @*/
    {
        int k = c;
        for (int i = 0; i < 1; ++i)
        /*@ inv 0i32 <= i; i <= 1i32;
            0i32 <= c; c < 1i32; // NOTE this is not the same as the outer invariant!
            k == c;
            {&k} unchanged;
            {&c} unchanged;
        @*/
        {
            /*@ assert(k==c);@*/
        }
        /*@ assert(k==c);@*/
    }
}

I think if the unchanged notation allowed {c} unchanged that would fix this.

% cn --version
git-b41bad6f9 [2025-03-13 16:25:31 +0000]

[dc-mak]

Seems related to #913

[dc-mak]

Please open new issues on www.github.com/rems-project/cn