0000624: Logging huge messages makes kernel crashing

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

Relationships

related to

0000623

closed

pascal

star_star dump

Relationships

Notes
~0001270 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.

~0002537 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"

~0002644 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. [...]

~0003877 yakobowski (manager) 2013-05-23 13:28	Fixed in Neon and onwards.

Notes

Date Modified	Username	Field	Change
Issue History
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

Issue History