E-ACSL crash with RTE generated assertion with booleans
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