ID0002417: **This issue was created automatically from Mantis Issue 2417. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002417 | Frama-C | Plug-in > E-ACSL | public | 2018-12-12 | 2020-06-12 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | rmalak | **Assigned To** | bdesloges | **Resolution** | fixed | | **Priority** | normal | **Severity** | major | **Reproducibility** | always | | **Platform** | x86_64 | **OS** | Linux 4.18 OCaml 4.07.0 | **OS Version** | Debian Sid | | **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | Frama-C 21-Scandium | ### Description : Hi, Don't know if this should go in E-ACSL or Kernel category. /////////////////// spaghetti.c int check(void) { return 0; } int main(void) { if( !check() || check() ) { goto mylabel; } mylabel: return 0; } //////////////////////// ### Additional Information : There is no problem in the following cases : * remove -e-acsl-full-mmodel * remove bracket * substitution "!check()" with "check()" * substitution "goto mylabel;" with "(void)0;" ### Steps To Reproduce : $ frama-c spaguetti.c -e-acsl -e-acsl-full-mmodel -then-last -print -ocode spaguetti.e-acsl.c [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing spaguetti.c (with preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". [kernel] User Error: Cannot find label for target of goto: _LOR: __e_acsl_store_block_duplicate((void *)(& tmp_0), (size_t)4); __e_acsl_delete_block((void *)(& tmp_0)); goto mylabel; ## Attachments - [spaguetti.c](/uploads/44b3cead438b8831534ab1b6ff6d6a15/spaguetti.c)