Just a guess, but perhaps they don't bother supporting 'unstructured switch' because they expect that input programs will most likely be written in the MISRA C

Just a guess, but perhaps they don't bother supporting 'unstructured switch' because they expect that input programs will most likely be written in the MISRA C subset of C anyway? I don't imagine it's due to technical challenges in formal modelling, as 'structured switch' statements still permit the default case to simply break immediately.