Inconsistent verification verdict with varying `--depth` value for `cbmc`

[jyoo980]

I am observing inconsistent verification verdicts from CBMC for the following function (entire source attached)

/* Try to get the number of columns in the current terminal. If the ioctl()
 * call fails the function will try to query the terminal itself.
 * Returns 0 on success, -1 on error. */
int getWindowSize(int ifd, int ofd, int *rows, int *cols)
__CPROVER_requires(__CPROVER_w_ok(rows, sizeof(*rows)))
__CPROVER_requires(__CPROVER_w_ok(cols, sizeof(*cols)))
__CPROVER_assigns(*rows, *cols)
__CPROVER_ensures(__CPROVER_return_value == 0 || __CPROVER_return_value == -1)
{
    struct winsize ws;

    if (ioctl(1, TIOCGWINSZ, &ws) == -1 || ws.ws_col == 0) {
        /* ioctl() failed. Try to query the terminal itself. */
        int orig_row, orig_col, retval;

        /* Get the initial position so we can restore it later. */
        retval = getCursorPosition(ifd,ofd,&orig_row,&orig_col);
        if (retval == -1) goto failed;

        /* Go to right/bottom margin and get position. */
        if (write(ofd,"\x1b[999C\x1b[999B",12) != 12) goto failed;
        retval = getCursorPosition(ifd,ofd,rows,cols);
        if (retval == -1) goto failed;

        /* Restore position. */
        char seq[32];
        snprintf(seq,32,"\x1b[%d;%dH",orig_row,orig_col);
        if (write(ofd,seq,strlen(seq)) == -1) {
            /* Can't recover... */
        }
        return 0;
    } else {
        *cols = ws.ws_col;
        *rows = ws.ws_row;
        return 0;
    }

failed:
    return -1;
}

Below are some results with running cbmc with varying depths:

• --depth 100: VERIFICATION SUCCESSFUL
• --depth 200: VERIFICATION SUCCESSFUL
• --depth 400
  • This yields the following error:

    **** WARNING: Depth-bounded analysis may yield unsound verification results
    CBMC version 6.7.1 (cbmc-6.7.1) 64-bit arm64 linux
    Reading GOTO program from file checking-getWindowSize-contracts.goto
    Generating GOTO Program
    Adding CPROVER library (arm64)
    Removal of function pointers and virtual functions
    Generic Property Instrumentation
    Starting Bounded Model Checking
    atomic sections differ across branches (at: file <builtin-library-write> line 48 function write)
    

• --depth 500: Same error as depth 400
• --depth 600: VERIFICATION SUCCESSFUL

Below is the set of commands I am using for verification:

goto-cc -o getWindowSize.goto kilo.c termios.c --function getWindowSize
goto-instrument --partial-loops --unwind 5 getWindowSize.goto getWindowSize.goto
goto-instrument --replace-call-with-contract getCursorPosition --enforce-contract getWindowSize getWindowSize.goto checking-getWindowSize-contracts.goto
cbmc checking-getWindowSize-contracts.goto --function getWindowSize --depth <DEPTH>

Can someone tell me whether this is expected behaviour? It seems surprising that verification verdicts change across depths (I would assume it would fail to verify for all depths past 400 if this is the case).

• kilo.c
• termios.c

Platform information

• CBMC 6.7.1