2021-01-25 15:22 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002417Frama-CPlug-in > E-ACSLpublic2018-12-12 15:082020-06-12 08:59
Reporterrmalak 
Assigned Tobdesloges 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
Platformx86_64OSLinux 4.18 OCaml 4.07.0OS VersionDebian Sid
Product VersionFrama-C 18-Argon 
Target VersionFixed in VersionFrama-C 21-Scandium 
Summary0002417: Invalid label with spaghetti code and E-ACSL full mmodel
DescriptionHi,

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 InformationThere is no problem in the following cases :

* remove -e-acsl-full-mmodel
* remove bracket
* substitution "!check()" with "check()"
* substitution "goto mylabel;" with "(void)0;"
TagsNo tags attached.
Attached Files
  • c file icon spaguetti.c (136 bytes) 2018-12-12 15:08 - 
    int check(void)
{
    return 0;
}
int main(void)
{
    if( !check() || check() ) {
        goto mylabel;
    }
mylabel:
    return 0;
}
    c file icon spaguetti.c (136 bytes) 2018-12-12 15:08 +

-Relationships
+Relationships

-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

Last edited: 2018-12-12 16:22

View 2 revisions

 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.
+Notes

-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
2020-06-12 08:59 signoles Status resolved => closed
+Issue History