0002417: Invalid label with spaghetti code and E-ACSL full mmodel

(0006700)
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); }

(0006701)
signoles (manager)
2018-12-12 16:17
edited on: 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; }

(0006702)
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).

(0006703)
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.

Issue History
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

Notes
(0006700) 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); }

(0006701) signoles (manager) 2018-12-12 16:17 edited on: 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; }

(0006702) 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).

(0006703) 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.

Relationships