+
+ // ToDo: The line below leads to the warning:
+ // warning: 'se.info.type' may be used uninitialized in this function
+ // This is caused by the fact that there are execution paths through the
+ // large switch statement above where some cases do not initialize this
+ // field. Is this really harmless? Can we avoid the warning?