Question: How to specify errno in a function contract's write set

[archigup]

How do we allow functions with contracts to modify the value of errno?

With the following:

#include <errno.h>

void foo(void) __CPROVER_assigns(errno) {
    errno = ENOMEM;
}

int main(void) {
    foo();
}

I get:

$ goto-cc test.c -o test.goto 
test.c: In function 'foo':
test.c:3:1: error: side-effects not allowed in assigns clause targets
 void foo(void) __CPROVER_assigns(errno) {
CONVERSION ERROR
1$

If I don't add errno to the assigns clause, I get verification failed with [foo.assigns.1] line 4 Check that *return_value___errno_location is assignable: FAILURE