[CN] _Noreturn function specifier does not work as expected

[peterohanley]

void _Noreturn exit(int status);
/*@
spec exit(i32 status);
requires true;
ensures true;
@*/
void _Noreturn exit1(int status)
{
}
void _Noreturn exit2(int status)
{
    exit(status);
}

% cn verify noreturn.c
[1/2]: exit1 -- fail
[2/2]: exit2 -- fail
noreturn.c:8:1: error: Undefined behaviour
void _Noreturn exit1(int status)
~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~ 
(UB missing short message): UB071_noreturn
State file: ...
noreturn.c:11:1: error: Undefined behaviour
void _Noreturn exit2(int status)
~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~ 
(UB missing short message): UB071_noreturn
State file: ...

Ok, both fail. exit1 is reasonable, it returns and it's marked _Noreturn. I think this is right and it matches the definition in undefined.lem.

In the state file for exit2 I see this:
Terms

term	value
call_exit0	{ .return = void }

This indicates exit has returned, even though it was marked _Noreturn. The UB happens in exit2 and not in exit as described in undefined.lem.

Is this happening because cerberus supports _Noreturn but CN doesn't?