setuid_spec() coverage

specification IntT setuid_spec( CallContext context, UidT uid, ErrorCode *errno )

coverages branches failures hits/fails
C ( Id, priority ) == ( Id_ReallyInvalid, Priority_ReallyHigh )   3
( Id, priority ) == ( Id_ReallyInvalid, Priority_ReallyLow )   3
( Id, priority ) == ( Id_ReallyInvalid, Priority_Unknown )   3
( Id, priority ) == ( Id_SavedSetId, Priority_ReallyHigh )   7
( Id, priority ) == ( Id_SavedSetId, Priority_ReallyLow ) failure 163: Requirement failed: {setuid.05.02} error not met because its predicate (( priority_coverage == Priority_ReallyLow || ( priority_coverage == Priority_Unknown && setuid_spec == -1 ) ) && ( uid_coverage != Id_RealId && uid_coverage != Id_SavedSetId )) is false while error code EPERM is set ;
4/1
( Id, priority ) == ( Id_SavedSetId, Priority_Unknown ) failure 164: Requirement failed: {setuid.05.02} error not met because its predicate (( priority_coverage == Priority_ReallyLow || ( priority_coverage == Priority_Unknown && setuid_spec == -1 ) ) && ( uid_coverage != Id_RealId && uid_coverage != Id_SavedSetId )) is false while error code EPERM is set ;
4/1
( Id, priority ) == ( Id_RealId, Priority_ReallyHigh )   6
( Id, priority ) == ( Id_RealId, Priority_ReallyLow )   2
( Id, priority ) == ( Id_RealId, Priority_Unknown )   2
( Id, priority ) == ( Id_Unknown, Priority_ReallyHigh )   1605
( Id, priority ) == ( Id_Unknown, Priority_ReallyLow )   6
( Id, priority ) == ( Id_Unknown, Priority_Unknown )   6
100% (12/12)   1652/2