Daniel Schwartz-Narbonne

Actually, would it make sense for the skip_write to return a `s2n_blob_slice`, so we carry around both the size, and the pointer together? https://github.com/awslabs/s2n/blob/0e74e54a14c4f48f95ebcb24cffd6690d0c11e4d/utils/s2n_blob.c#L55

"We might need to communicate socket readiness - and potentially the amount of buffered bytes inside S2N - in a side channel." Why not just add an extra `uint32_t *num_buffered_bytes_out`...

[memcpy_issue.zip](https://github.com/smackers/smack/files/1616656/memcpy_issue.zip)

Thanks

We should support the examples from https://doc.rust-lang.org/stable/std/mem/union.MaybeUninit.html

Why not create a poison expression, that translates to nondet plus comment when you lower to irep?

@RalfJung I'm not totally sure about this. From the `C` Standard: > If an argument to a function has an invalid value (such as a value outside the domain of...

It looks like if I declare the `dangling` pointer as a 0 byte allocated region using the `mmio` flag to CBMC it works as expected: ```C // cbmc mmio.c --mmio-regions...

@tautschnig may have thoughts on the semantics of `C` pointers

Similarly > [2](http://port70.net/~nsz/c/c11/n1570.html#7.24.1p2) Where an argument declared as size_t n specifies the length of the array for a function, n can have the value zero on a call to that...