CN: add ghost arguments

[cassiatorczon]

Motivating example: C string operations that require knowing the size of the available buffer (e.g., for concatenation by copying the second string into the unused space in the buffer of the first string). The buffer size isn't passed as an argument to the C function, but it's necessary for the spec and (if the function is being used safely) is known at the call site

[dc-mak]

Any motivating examples? Would be good for having test cases :-)