Internal error "Bytes.create"

When trying to test this example, I encountered:

#include <stdlib.h>

typedef int VEC_ELEMENT;

struct Vector {
  int size;
  int capacity;
  VEC_ELEMENT *data;
};

void *cn_malloc(size_t size);
void cn_free_sized(void *ptr, size_t size);

/*@

type_synonym VEC_ELEMENT = i32

type_synonym Vec = { i32 size, i32 capacity, map<i32,VEC_ELEMENT> elements }

predicate (Vec) Vec(pointer p) {
  take node = Owned<struct Vector>(p);
  assert(0i32 <= node.size);
  assert(node.size <= node.capacity);
  take used = each(i32 i; 0i32 <= i && i < node.size) {
    Owned<VEC_ELEMENT>(array_shift<VEC_ELEMENT>(p,i))
  };
  take unused = each(i32 i; node.size <= i && i < node.capacity) {
    Block<VEC_ELEMENT>(array_shift<VEC_ELEMENT>(p,i))
  };
  return { size: node.size, capacity: node.capacity, elements: used };
} 
@*/

// capacity >= size
void vec_resize(struct Vector *vec, int capacity)
/*@
requires
  take xs = Vec(vec);
  xs.size <= capacity;
ensures
  take ys = Vec(vec);
  ys.capacity == capacity;
  xs.elements == ys.elements;
@*/
{
  VEC_ELEMENT *new_data = (VEC_ELEMENT*) cn_malloc(sizeof(VEC_ELEMENT) * capacity);
  size_t i = 0;
  while (i < vec->size) {
    new_data[i] = vec->data[i];
    ++i;
  }
  cn_free_sized(vec->data, sizeof(VEC_ELEMENT) * vec->capacity);
  vec->data = new_data;
  vec->capacity = capacity;
}

cn: internal error, uncaught exception:
    Invalid_argument("Bytes.create")
    Raised by primitive operation at Stdlib.really_input_string in file "stdlib.ml", line 439, characters 10-26

CN version:

git-368d51a1f [2024-11-05 10:05:01 -0500]

Note that spec for Vec is incorrect as the ownership should be related to the data stored in the vector. Despite that we shouldn't really crash here.

rems-project / cerberus

Internal error "Bytes.create" #698