I found (what I believe is) a small typo in the Starterware software.
In the file interrupt.c there is this subroutine (here given simply as pseudo-code), with the culprit in red. The '3' should be a '4', as there are four pairs of registers to be initialized. It might perhaps happen (by chance) to be safe, nonetheless it strikes me as unclean, as it leaves one pair of registers uninitialized, (ECR4 and SECR4).
IntAINTCInit()
{
/* Reset AINTC */
for(cnt = 0; cnt < 3; cnt++)
{
HWREG(SOC_AINTC_0_REGS + AINTC_ECR(cnt)) = AINTC_ECR_DISABLE;
HWREG(SOC_AINTC_0_REGS + AINTC_SECR(cnt)) = AINTC_SECR_ENBL_STATUS;
}
...
}
