Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 201
    • Issues 201
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #514
Closed
Open
Created Mar 18, 2016 by mantis-gitlab-migration@mantis-gitlab-migration

Crash with large array initialisation

ID0002219: This issue was created automatically from Mantis Issue 2219. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002219 Frama-C Plug-in > wp public 2016-03-18 2016-03-22
Reporter szt Assigned To correnson Resolution open
Priority normal Severity crash Reproducibility always
Platform x86-64 OS GNU/Linux OS Version Ubuntu 14.04.4
Product Version Frama-C Magnesium Target Version - Fixed in Version -

Description :

wp plugin crashes when I try to check code

Additional Information :

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] Parsing ../../prog/array_testcase.c (with preprocessing) [kernel] Current source was: ../../prog/array_testcase.c:1 The full backtrace is: Raised at file "src/plugins/wp/register.ml", line 607, characters 30-32 Called from file "queue.ml", line 134, characters 6-20 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 778, characters 2-9 Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 227, characters 4-8

     Unexpected error (Stack overflow).
     Please report as 'crash' at http://bts.frama-c.com/.
     Your Frama-C version is Magnesium-20151002.
     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

Steps To Reproduce :

just run frama-c -wp -wp-proof alt-ergo array_testcase.c

Attachments

  • array_testcase.c
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking