View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000624 | Frama-C | Kernel | public | 2010-11-10 17:04 | 2014-03-13 15:57 | ||||
Reporter | teamod | ||||||||
Assigned To | correnson | ||||||||
Priority | urgent | Severity | crash | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Boron-20100401 | ||||||||
Target Version | Frama-C Neon-20140301 | Fixed in Version | Frama-C Neon-20140301 | ||||||
Summary | 0000624: Logging huge messages makes kernel crashing | ||||||||
Description | The environment is exactly the same as described in 0000623, below is the output. [kernel] The full backtrace is: Raised by primitive operation at file "src/kernel/log.ml", line 201, characters 9-24 Called from file "format.ml", line 299, characters 4-28 Called from file "format.ml", line 428, characters 6-72 Called from file "format.ml", line 435, characters 6-24 Called from file "format.ml", line 1152, characters 8-28 Called from file "format.ml", line 1157, characters 10-25 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "external/ptmap.ml", line 153, characters 3-15 Called from file "format.ml", line 1157, characters 10-25 Called from file "format.ml", line 1157, characters 10-25 Called from file "format.ml", line 1157, characters 10-25 Called from file "src/memory_state/offsetmap.ml", line 265, characters 6-66 Called from file "src/lib/rangemap.ml", line 172, characters 20-25 Called from file "format.ml", line 1157, characters 10-25 Called from file "format.ml", line 1157, characters 10-25 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "external/ptmap.ml", line 535, characters 16-35 Called from file "src/memory_state/lmap.ml", line 290, characters 4-43 Called from file "src/memory_state/relations_type.ml", line 750, characters 4-43 Called from file "format.ml", line 1157, characters 10-25 Called from file "queue.ml", line 134, characters 6-20 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 50, characters 4-20 Called from file "src/kernel/cmdline.ml", line 170, characters 4-8 Unexpected error (Invalid_argument("String.create")). Please report as 'crash' at http://bts.frama-c.com | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
pascal (reporter) 2010-11-12 14:09 |
The crash is in the message-printing module. I guess that module should never request the creation of a string of length more than Sys.max_string_length, and display an explanation together with the beginning of the message being composed when it finds itself about to do so. You can circumvent the problem with option -quiet. Also, you can circumvent the problem by using the 64-bit version of Frama-C, where Sys.max_string_length is larger than you have memory for, but since we do not know what the message is and it's already unreasonably long, it may also fill your memory completely. The -quiet solution seems a better bet. |
pascal (reporter) 2011-12-09 06:20 |
Backtrace rapportée par Stéphane Duprat le 9 décembre 2011: kernel] The full backtrace is: Raised by primitive operation at file "src/kernel/log.ml", line 197, characters 16-31 Called from file "format.ml", line 428, characters 6-72 Called from file "format.ml", line 435, characters 6-24 Called from file "format.ml", line 1145, characters 10-28 Called from file "src/memory_state/cvalue.ml", line 274, characters 12-44 Called from file "format.ml", line 1154, characters 10-25 Called from file "src/memory_state/offsetmap.ml", line 253, characters 6-66 Called from file "src/lib/rangemap.ml", line 234, characters 16-21 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "src/lib/rangemap.ml", line 234, characters 6-14 Called from file "format.ml", line 1154, characters 10-25 Called from file "format.ml", line 1154, characters 10-25 Called from file "external/hptmap.ml", line 201, characters 3-15 Called from file "external/hptmap.ml", line 201, characters 3-15 Called from file "src/memory_state/lmap.ml", line 352, characters 9-241 Called from file "format.ml", line 1154, characters 10-25 Called from file "src/value/eval_funs.ml", line 421, characters 6-136 Called from file "src/value/eval_funs.ml", line 554, characters 11-44 Re-raised at file "src/value/eval_funs.ml", line 570, characters 47-50 Called from file "src/project/state_builder.ml", line 1076, characters 9-13 Re-raised at file "src/project/state_builder.ml", line 1080, characters 15-18 Called from file "src/value/register.ml", line 46, characters 4-24 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 723, characters 2-9 Called from file "src/kernel/cmdline.ml", line 200, characters 4-8 Unexpected error (Invalid_argument("String.create")). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Nitrogen-20111001. Note that a version and a backtrace alone often does not have 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 [kernel] saving the current session into file "frama-c/out/IBU_Se_WriteUpdateObject.frm" |
correnson (manager) 2012-01-30 12:58 |
This was temporary fixed in 17078, but the solution is not complete. Messages larger than 262144 bytes are truncated with an ellipsis ("...") in the *middle* of the message. This limit is not (yet) modifiable by command-line option. From my point of view, this limit is still too large. This hight limit prevent some tests oracles from being truncated (cruise-control for instance). But I still think that producing large messages with 'MyPlugin.result' is a not a good idea. Things to discuss or do: - adding a command line option for the limit - remove 'MyPlugin.result' - make 'MyPlugin.result' to dump messages in console, like Log.print_delayed / Log.print_on_output, without emitting a recorded event message (no limit applies). - keep 'MyPlugin.result' and add 'MuPlugin.bigresult' for this purpose. - modify all plugins that output large messages and make them use Log.print_delayed instead of MyPlugin.result. [...] |
yakobowski (manager) 2013-05-23 13:28 |
Fixed in Neon and onwards. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2010-11-10 17:04 | teamod | New Issue | |
2010-11-10 17:53 | signoles | Assigned To | => pascal |
2010-11-10 17:53 | signoles | Status | new => assigned |
2010-11-10 17:53 | signoles | Category | Kernel => Plug-in > value analysis |
2010-11-10 17:57 | signoles | Relationship added | related to 0000623 |
2010-11-12 14:05 | pascal | Assigned To | pascal => correnson |
2010-11-12 14:09 | pascal | Note Added: 0001270 | |
2010-12-13 14:55 | correnson | Status | assigned => acknowledged |
2010-12-13 14:55 | correnson | Category | Plug-in > value analysis => Kernel |
2010-12-13 14:55 | correnson | Target Version | => Frama-C Carbon-20110201 |
2010-12-13 14:55 | correnson | Summary | Frama finally crashes in the issues of 0000623 => Logging huge messages makes kernel crashing |
2011-02-02 10:39 | correnson | Target Version | Frama-C Carbon-20110201 => Frama-C Nitrogen-20110901 |
2011-09-30 13:42 | correnson | Target Version | Frama-C Nitrogen-20111001 => Frama-C Oxygen-2012xx01 |
2011-12-09 06:20 | pascal | Note Added: 0002537 | |
2012-01-30 12:58 | correnson | Note Added: 0002644 | |
2012-09-11 11:53 | signoles | Target Version | Frama-C Oxygen-2012xx01 => |
2012-12-17 14:02 | yakobowski | Priority | normal => urgent |
2012-12-17 14:02 | yakobowski | Target Version | => Frama-C Fluorine |
2013-04-16 09:48 | svn | ||
2013-04-17 08:53 | signoles | Target Version | Frama-C Fluorine => Frama-C Neon-20140301 |
2013-05-23 13:28 | yakobowski | Note Added: 0003877 | |
2013-05-23 13:28 | yakobowski | Status | acknowledged => resolved |
2013-05-23 13:28 | yakobowski | Resolution | open => fixed |
2013-05-23 17:07 | signoles | Fixed in Version | => Frama-C Fluorine-20130501 |
2013-05-23 17:07 | signoles | Status | resolved => closed |
2013-05-23 17:15 | signoles | Status | closed => resolved |
2013-05-23 17:15 | signoles | Fixed in Version | Frama-C Fluorine-20130501 => |
2013-12-19 01:11 | yakobowski | Source_changeset_attached | => framac master 381dd14a |
2014-02-12 16:53 | yakobowski | Source_changeset_attached | => framac stable/neon 381dd14a |
2014-03-13 15:56 | signoles | Fixed in Version | => Frama-C Neon-20140301 |
2014-03-13 15:57 | signoles | Status | resolved => closed |