Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000624Frama-CKernelpublic2010-11-10 17:042014-03-13 15:57
Reporterteamod 
Assigned Tocorrenson 
PriorityurgentSeveritycrashReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFrama-C Neon-20140301Fixed in VersionFrama-C Neon-20140301 
Summary0000624: Logging huge messages makes kernel crashing
DescriptionThe 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 [^]
TagsNo tags attached.
Attached Files

- Relationships
related to 0000623closedpascal star_star dump 

-  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.

- Issue History
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-02-02 10:43 signoles Relationship added related to 0000232
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 Checkin
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 =>
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker