ID0002412: **This issue was created automatically from Mantis Issue 2412. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002412 | Frama-C | Plug-in > E-ACSL | public | 2018-12-03 | 2018-12-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | rmalak | **Assigned To** | signoles | **Resolution** | open | | **Priority** | normal | **Severity** | crash | **Reproducibility** | always | | **Platform** | x86_64 | **OS** | Linux x86_64 | **OS Version** | Debian Sid | | **Product Version** | Frama-C 18-Argon | **Target Version** | - | **Fixed in Version** | - | ### Description : There might be a regression with the RTE or E-ACSL plugin with Argon. /////////// boolean.c #include <stdbool.h> bool return_false(void) { return false; } int main(void) { return 0; } /////////////////////////// ### Additional Information : On Chlorine-20180502 (bfd93b819) : $ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c [kernel] Parsing boolean.c (with preprocessing) [rte] annotating function main [rte] annotating function return_false $ frama-c -machdep x86_64 rte_boolean.c -e-acsl [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing rte_boolean.c (with preprocessing) [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". ### Steps To Reproduce : On Argon 18.0 (2f7a0eee0) : $ frama-c -machdep x86_64 boolean.c -rte -print -ocode rte_boolean.c [kernel] Parsing boolean.c (with preprocessing) [rte] annotating function main [rte] annotating function return_false $ frama-c -machdep x86_64 rte_boolean.c -e-acsl [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl_gmp_api.h (with preprocessing) [kernel] Parsing local-frama-c/share/frama-c/e-acsl/e_acsl.h (with preprocessing) [kernel] Parsing rte_boolean.c (with preprocessing) [e-acsl] beginning translation. [kernel] Current source was: rte_boolean.c:10 The full backtrace is: Raised at file "src/libraries/project/project.ml", line 402, characters 50-57 Called from file "src/plugins/e-acsl/main.ml", line 155, characters 12-1023 Called from file "src/plugins/e-acsl/main.ml", line 121, characters 12-34 Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22 Called from file "src/plugins/e-acsl/main.ml", line 255, characters 11-56 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 822, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8 Unexpected error (Stack overflow). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is 18.0 (Argon). Note that a version and a backtrace alone often do not contain enough information to understand the bug. Guidelines for reporting bugs are at: http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines ## Attachments - [boolean.c](/uploads/1b34c066b4dc860013dcc10c38a49aad/boolean.c)