[CN] cannot create pointers past the end of arrays passed as parameters

[peterohanley]

void param(int *a, unsigned long l)
/*@
  requires take ai = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
  ensures take ao = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
@*/
{
    int b[1];
    int *q = b+1;
    int *p = a+1;
}

% cn verify past_the_end.c
[1/1]: param -- fail
past_the_end.c:9:14: error: Pointer `&a[(u64)1'i32]` out of bounds
    int *p = a+1;
             ~^~ 
(UB missing short message): UB_CERB004_unspecified__pointer_add

I think both are valid one-past-the-end pointers, but I don't have a spec reference for it.

This might be a VIP thing.

[peterohanley]

I have better examples:

#include <stdint.h>

void param1(int *a, unsigned long l)
/*@
  requires
  take ai = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
  l > 0u64;
  ensures take ao = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
@*/
{
    uintptr_t a_ = (uintptr_t)a;
    /*@ extract Owned<int>, 0u64; @*/
    int *p = __cerbvar_copy_alloc_id(a_+0, a);
}

void param2(int *a, unsigned long l)
/*@
  requires
  take ai = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
  l > 0u64;
  ensures take ao = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
@*/
{
    /*@ extract Owned<int>, 0u64; @*/
    int *p = __cerbvar_copy_alloc_id(((uintptr_t)a)+0, a);
}

void param3(int *a, unsigned long l)
/*@
  requires
  take ai = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
  ensures take ao = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
@*/
{
    // can't extract anymore
    int *p = __cerbvar_copy_alloc_id(((uintptr_t)a)+l, a);
}

void param4(int *a, unsigned long l)
/*@
  requires
  take ai = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
  l > 0u64;
  ensures take ao = each(u64 i; i >= 0u64 && i < l) {Owned<int>(array_shift<int>(a,i))};
@*/
{
    /*@ extract Owned<int>, 0u64; @*/
    int *p = __cerbvar_copy_alloc_id(((uintptr_t)a)+l, a);
}

% cn verify copy_alloc_id.c
[1/4]: param1 -- pass
[2/4]: param2 -- pass
[3/4]: param3 -- fail
[4/4]: param4 -- fail
copy_alloc_id.c:36:14: error: Pointer `a` needs to be live for copy_alloc_id
    int *p = __cerbvar_copy_alloc_id(((uintptr_t)a)+l, a);
             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
Need an Alloc or Owned in context with same allocation id
State file: file:///var/folders/tz/g0kxkm2915xdtm6qgv8rff000000gp/T/state__copy_alloc_id.c__param3.html
copy_alloc_id.c:48:14: error: Undefined behaviour
    int *p = __cerbvar_copy_alloc_id(((uintptr_t)a)+l, a);
             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
(UB missing short message): UB_CERB004_unspecified__copy_alloc_id
State file: file:///var/folders/tz/g0kxkm2915xdtm6qgv8rff000000gp/T/state__copy_alloc_id.c__param4.html

param3 doesn't work because we might not have any access at a, but I think a pointer past the end of a zero-length array is valid. It might only be valid if the array is a flexible struct member though.

param4 doesn't work, I don't understand why.

[dc-mak]

These are all VIP related. I'll take a look next week.