View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002417 | Frama-C | Plug-in > E-ACSL | public | 2018-12-12 15:08 | 2020-06-12 08:59 | ||||
Reporter | rmalak | ||||||||
Assigned To | bdesloges | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
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 | |||||||
Summary | 0002417: Invalid label with spaghetti code and E-ACSL full mmodel | ||||||||
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; } //////////////////////// | ||||||||
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; | ||||||||
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;" | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 2018-12-12 16:09 |
Thank you for the precise bug report. That is definitely a bug when monitoring memory locations in presence of some "special" gotos. To myself: here is a minimal example that reproduces the bug without using -e-acsl-full-mmodel. int main(void) { if (0) { int x; if (0) _LOR: /*@ assert \valid(&x); */ ; } else goto _LOR; return 0; } $ frama-c a.c -check -e-acsl [e-acsl] beginning translation. [kernel] a.c:12: Failure: [AST Integrity Check] AST of e-acsl Statement is referenced by \at or goto without having a label: /*@ assert \valid(&x); */ { int __gen_e_acsl_valid; __gen_e_acsl_valid = __e_acsl_valid((void *)(& x),sizeof(int), (void *)(& x),(void *)0); __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main", (char *)"\\valid(&x)",6); _LOR: __e_acsl_store_block_duplicate((void *)(& x),(size_t)4); } |
signoles (manager) 2018-12-12 16:17 Last edited: 2018-12-12 16:22 |
Even simpler example: the crash arises when handling the local inside the block in which the goto goes back. int main(void) { { int x; _LOR: /*@ assert \valid(&x); */ ; } goto _LOR; return 0; } |
signoles (manager) 2018-12-12 16:21 |
To rmallac: a workaround consists in moving the calls to check outside the conditional. (I know that modifying the code is not fully satisfactory, but at least it solves your issue while waiting a bug fix). |
rmalak (reporter) 2018-12-12 16:25 |
In my use-case (Contiki-NG), I changed temporary a if (!A||!B) into a if (!(A&&B)) in 2 places in the code. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2018-12-12 15:08 | rmalak | New Issue | |
2018-12-12 15:08 | rmalak | Status | new => assigned |
2018-12-12 15:08 | rmalak | Assigned To | => signoles |
2018-12-12 15:08 | rmalak | File Added: spaguetti.c | |
2018-12-12 16:09 | signoles | Note Added: 0006700 | |
2018-12-12 16:09 | signoles | Status | assigned => confirmed |
2018-12-12 16:17 | signoles | Note Added: 0006701 | |
2018-12-12 16:21 | signoles | Note Added: 0006702 | |
2018-12-12 16:22 | signoles | Note Edited: 0006701 | View Revisions |
2018-12-12 16:25 | rmalak | Note Added: 0006703 | |
2020-03-20 12:23 | signoles | Assigned To | signoles => bdesloges |
2020-03-20 12:23 | signoles | Status | confirmed => assigned |
2020-03-20 15:06 | bdesloges | Status | assigned => resolved |
2020-03-20 15:06 | bdesloges | Fixed in Version | => Frama-C 21-Scandium |
2020-03-20 15:06 | bdesloges | Resolution | open => fixed |
2020-06-12 08:59 | signoles | Status | resolved => closed |