CN: Array shift should not crash on void* pointer

[dc-mak]

15:46 ➜  cerberus git:(main) cn verify cn_crash.c
internal error: size_of_ctype applied to void
cn: internal error, uncaught exception:
    Failure("internal error: size_of_ctype applied to void")
    Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
    Called from Cn__WellTyped.WIT.infer in file "backend/cn/lib/wellTyped.ml", line 773, characters 17-40
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure.(fun) in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure.(fun) in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.pure.(fun) in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure.(fun) in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.pure.(fun) in file "backend/cn/lib/typing.ml", line 76, characters 22-25
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.bind.(fun) in file "backend/cn/lib/typing.ml", line 49, characters 17-20
    Called from Cn__Typing.run_to_pause in file "backend/cn/lib/typing.ml", line 64, characters 8-21
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 165, characters 8-85
    Called from Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", lines 157-168, characters 6-48
    Re-raised at Dune__exe__Main.with_well_formedness_check in file "backend/cn/bin/main.ml", line 176, characters 4-69
    Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
    Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
15:46 ➜  cerberus git:(main) cat cn_crash.c
#include <stdlib.h>
#include <string.h>

void *_malloc(size_t size)
/*@ trusted;
ensures
  take A = Alloc(return);
  A.base == (u64) return;
  A.size == size;
  take B = each(u64 i; i < size) {Block<unsigned char>(array_shift(return, i))};
@*/
{
    return malloc(size);
}