Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #520

FRama C Nitrogen Nitrogen-20111001

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


Id Project Category View Due Date Updated
ID0002210 Frama-C Plug-in > pdg public 2016-02-22 2016-02-25
Reporter lammyday Assigned To yakobowski Resolution unable to reproduce
Priority normal Severity crash Reproducibility sometimes
Platform - OS Linux OS Version Ubuntu 14.04
Product Version Frama-C GIT, precise the release id Target Version - Fixed in Version -

Description :

Frama-c pdg crashed of an unexpected error(out of memeory) after a warning that it could not find a final state, or a final state was unreachable.

Additional Information :

Error meesages from crash:

main.c:2313:[pdg] warning: no final state. Probably unreachable... [pdg] done for function main [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 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 1148, characters 10-28 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 "external/hptmap.ml", line 201, characters 3-15 Called from file "external/hptmap.ml", line 201, characters 3-15 Called from file "list.ml", line 69, characters 12-15 Called from file "src/pdg_types/pdgTypes.ml", line 584, characters 6-33 Called from file "format.ml", line 1157, characters 10-25 Called from file "format.ml", line 1157, characters 10-25 Called from file "src/pdg/register.ml", line 140, characters 8-63 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/pdg/register.ml", line 145, characters 4-68 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 (Out of memory).
     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

Steps To Reproduce :

execute: "frama-c -pdg -dot-pdg graph -pdg-print main.i -main main -val-ignore-recursive-calls"

on the make gnu utility with git version: 036760a9fdb11849b6a43feec7ce294e7f77db2a this is obtainable from this url: http://git.savannah.gnu.org/cgit/make.git/snapshot/make-036760a9fdb11849b6a43feec7ce294e7f77db2a.tar.gz

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