ID0001502: **This issue was created automatically from Mantis Issue 1502. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001502 | Frama-C | Kernel | public | 2013-10-16 | 2014-03-13 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | dpariente | **Assigned To** | virgile | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Fluorine-20130601 | **Target Version** | - | **Fixed in Version** | Frama-C Neon-20140301 | ### Description : [STANCE] The following code: void f(int a) { goto _LOR_0; if (a) _LOR_0: ; } analyzed by: frama-c ../skip.c -print -ocode ../skip2.c (with or without -no-simplify-cfg) generates a warning: [kernel] user error: Label _LOR_0 not found and an error when parsing pretty-printed code in skip2.c: frama-c ../skip2.c [kernel] user error: Label _LOR_0 not found It seems that the branch containing the label is pruned as considered as empty! Typically, modifying cabs2cil.ml (line 1142) so that Instr (Skip _) is no more considered as an empty stmt solves the problem (of course this is just a workaround!). Is something more robust available? ## Attachments - [bts1502.patch](/uploads/9d5770006929f966bf768c169c8c6b21/bts1502.patch)