Crash when trying to analyse a file with jessie
ID0002334: This issue was created automatically from Mantis Issue 2334. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002334 | Frama-C | Plug-in > jessie | public | 2017-12-06 | 2018-07-11 |
| Reporter | abustany | Assigned To | cmarche | Resolution | fixed |
| Priority | normal | Severity | crash | Reproducibility | always |
| Platform | x86_64 | OS | Linux | OS Version | 4.7.9 |
| Product Version | Frama-C 15-Phosphorus | Target Version | - | Fixed in Version | Frama-C 17-Chlorine |
Description :
When running "frama-c -jessie jessie-crash.c" on the attached file, I get the following crash:
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing encoding.c (with preprocessing) [jessie] Starting Jessie translation [jessie] warning: \separated is not supported by Jessie. This predicate will be ignored [kernel] Current source was: FRAMAC_SHARE/libc/__fc_string_axiomatic.h:35 The full backtrace is: Raised at file "interp.ml", line 2383, characters 5-24 Called from file "interp.ml", line 2644, characters 22-41 Called from file "list.ml", line 70, characters 22-25 Called from file "interp.ml", line 2731, characters 27-66 Called from file "register.ml", line 175, characters 16-32 Called from file "register.ml", line 278, characters 6-12 Re-raised at file "register.ml", line 251, characters 29-103 Called from file "queue.ml", line 105, characters 6-15 Called from file "src/kernel_internals/runtime/boot.ml", line 37, characters 4-20 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 789, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 819, characters 18-64 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 228, characters 4-8
Unexpected error (File "interp.ml", line 2383, characters 5-11: Assertion failed).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Phosphorus-20170501.
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_guidelinesMy packages are at the following version:
frama-c 20170501 why 2.39 why3 0.87.3 ocaml 4.03.0