typedef unsigned char uint8_t;
typedef struct s {
    uint8_t a;
} s;
/*@
predicate (map<u64,u8>) Array_u8 (pointer p, u64 l)
{
  take pv = each(u64 i; i >= 0u64 && i < l) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
  return pv;
}
@*/

#if 0
static void transmute_to_blob(void *p)
/*@
  requires take xsi = Array_u8(p, sizeof<s>);
  ensures take xso = Owned<s>(p);
  @*/
{
  /*@ from_bytes Owned<s>(p); @*/
}
#else

static void untransmute_to_blob(void *p)
/*@
  requires take xsi = Owned<s>(p);
  ensures take xso = Array_u8(p, sizeof<s>);
  @*/
{
  /*@ to_bytes Owned<s>(p); @*/
}
#endif

% cn verify to_bytes.c
to_bytes.c:30:7: warning: experimental keyword 'to_bytes' (use of experimental features is discouraged)
  /*@ to_bytes Owned<s>(p); @*/
      ^~~~~~~~ 
cn: internal error, uncaught exception:
    File "backend/cn/lib/check.ml", line 1866, characters 74-80: Assertion failed
    Raised at Cn__Check.check_expr.bytes_constraints in file "backend/cn/lib/check.ml", line 1866, characters 74-86
...

% cn verify to_bytes.c
to_bytes.c:20:7: warning: experimental keyword 'from_bytes' (use of experimental features is discouraged)
  /*@ from_bytes Owned<s>(p); @*/
      ^~~~~~~~~~ 
cn: internal error, uncaught exception:
    File "backend/cn/lib/check.ml", line 1866, characters 74-80: Assertion failed
    Raised at Cn__Check.check_expr.bytes_constraints in file "backend/cn/lib/check.ml", line 1866, characters 74-86
...