Invalid label with spaghetti code and E-ACSL full mmodel
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;