invariant violation report using loop contracts

[polgreen]

CBMC version: 5.90.0 (cbmc-5.90.0-21-g6590981c4a
Operating system: MacOS 14.6.1
Exact command line resulting in the issue:

goto-cc tmp.c
goto-instrument --apply-loop-contracts  a.out b.o

File tmp.c:

int main()
{

    int rows=3;
    int cols = 3;

    int* arr = malloc(rows * cols * sizeof(int));
    int *idx = &arr[0];

    for(int i=0; i<rows; i++)
    __CPROVER_loop_invariant(0 <= i && i <= rows)
    __CPROVER_loop_invariant(idx == &arr[0]+i*rows)
    __CPROVER_loop_invariant(rows==3 && cols==3)
    {
         for(int j=0; j<cols; j++)
         __CPROVER_loop_invariant(0 <= j && j <= cols)
         __CPROVER_loop_invariant(idx == &arr[0]+i*j)
         {
            *idx = i*j;
            idx++;
         }

    }
    return 1;
}

What behaviour did you expect: Not an invariant violation

What happened instead:

--- begin invariant violation report ---
Invariant check failed
File: local_may_alias.cpp:120 function: get
Condition: loc_it != cfg.loc_map.end()
Reason: Check return value
Backtrace:
0   goto-instrument                     0x0000000100bb7daa _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 74
1   goto-instrument                     0x0000000100bb8608 _Z13get_backtracev + 184
2   goto-instrument                     0x0000000100803a9c _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 44
3   goto-instrument                     0x00000001008039c9 _Z25invariant_violated_stringRKNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEES7_iS7_S7_ + 9
4   goto-instrument                     0x0000000100b640e9 _ZNK16local_may_aliast3getENSt3__121__list_const_iteratorIN13goto_programt12instructiontEPvEERK5exprt + 377
5   goto-instrument                     0x0000000100e2c971 _Z15get_assigns_lhsRK16local_may_aliastNSt3__121__list_const_iteratorIN13goto_programt12instructiontEPvEERK5exprtRNS2_3setIS8_NS2_4lessIS8_EENS2_9allocatorIS8_EEEE + 257
6   goto-instrument                     0x0000000100e2cd18 _Z11get_assignsRK16local_may_aliastRK14loop_templatetINSt3__115__list_iteratorIN13goto_programt12instructiontEPvEENS6_16target_less_thanEERNS3_3setI5exprtNS3_4lessISE_EENS3_9allocatorISE_EEEE + 120
7   goto-instrument                     0x0000000100d4aa97 _ZN15code_contractst26check_apply_loop_contractsERK8dstringtR14goto_functiontRK16local_may_aliastNSt3__115__list_iteratorIN13goto_programt12instructiontEPvEESD_RK14loop_templatetISD_NSB_16target_less_thanEE5exprtSJ_SJ_S2_ + 2423
8   goto-instrument                     0x0000000100d51b54 _ZN15code_contractst19apply_loop_contractERK8dstringtR14goto_functiont + 6372
9   goto-instrument                     0x0000000100d564bd _ZN15code_contractst20apply_loop_contractsERKNSt3__13setINS0_12basic_stringIcNS0_11char_traitsIcEENS0_9allocatorIcEEEENS0_4lessIS7_EENS5_IS7_EEEE + 413
10  goto-instrument                     0x0000000100e0248c _ZN30goto_instrument_parse_optionst23instrument_goto_programEv + 7900
11  goto-instrument                     0x0000000100dfd3f4 _ZN30goto_instrument_parse_optionst4doitEv + 836
12  goto-instrument                     0x0000000100bebf3f _ZN19parse_options_baset4mainEv + 143
13  goto-instrument                     0x0000000100dfcd68 main + 40
14  dyld                                0x0000000201426345 start + 1909


--- end invariant violation report ---

[remi-delmas-3000]

Thanks for reporting the issue.

Here's a version of the contracts that pass verification:

#include <assert.h>
#include <stdlib.h>
#include <stdio.h>
int main()
{

    int rows = 3;
    int cols = 3;

    int *arr = malloc(rows * cols * sizeof(int));
    if(arr == NULL)
       return -1;
    int* idx = &arr[0];

    for (int i = 0; i < rows; i++)
    __CPROVER_assigns(i, idx,  __CPROVER_object_whole(idx))
    __CPROVER_loop_invariant(0 <= i && i <= rows)
    __CPROVER_loop_invariant(idx == (&arr[0] + i * cols))
    {
        for(int j = 0; j < cols; j++)
        __CPROVER_assigns(j, idx,  __CPROVER_object_whole(idx))
        __CPROVER_loop_invariant(0 <= j && j <= cols)
        __CPROVER_loop_invariant(idx == (&arr[0] + i * cols + j))
        {
            *idx = i*j;
            idx++;
        }
    }
    return 0;
}