[CN] Array example fails when using size_t index (but passes with unsigned long)

[septract]

CN fails to verify an array access when using an index of type size_t, but passes the same example when the index has type unsigned long (size_t is an alias for unsigned long, at least on my system).

Replication

The following example fails in CN:

#include <stddef.h>
#define MAX_LEN 32
static int eg1[MAX_LEN];
static size_t eg1_len = 0; // <-- Use `size_t` here 

void mem_access_eg1_fail() 
/*$
accesses eg1; 
accesses eg1_len; 
$*/
{
    if (eg1_len >= MAX_LEN)
        return;
    int* p = &eg1[eg1_len];
}

The example fails with the following error:

  $ cn verify --magic-comment-char-dollar global_mem_2.c --output=debug
  [1/2]: mem_access_eg1_fail -- fail
  [2/2]: mem_access_eg2_pass -- pass
  global_mem_2.c:20:14: error: `&(&&eg1[(u64)0'i32])[O_eg1_len0]` out of bounds
      int* p = &eg1[eg1_len];
              ^~~~~~~~~~~~~ 
  (UB missing short message): UB_CERB004_unspecified__pointer_add

However, the same example works when the type of the index is changed unsigned long:

// Example passes w `unsigned long` 
#include <stddef.h>
#define MAX_LEN 32
static int eg2[MAX_LEN];
static unsigned long eg2_len = 0; // <-- use `unsigned long` here 

void mem_access_eg2_pass() 
/*$
accesses eg2; 
accesses eg2_len; 
$*/
{
    if (eg2_len >= MAX_LEN)
        return;
    int* p = &eg2[eg2_len];
}

Analysis

• @peterohanley pointed to another example of anomalous behavior with size_t: [CN] cannot use prefix increment with size_t in a loop #678
• This issue may be addressed by Adding a switch for normalising types at elaboration time #805, per the discussion on that PR.
• We need this for the MKM OpenSUT example, see example code here.