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
  • #497

Crash when running "frama-c -jessie -jessie-atp=gui reduce.c"

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


Id Project Category View Due Date Updated
ID0001790 Frama-C Plug-in > jessie public 2014-05-29 2016-06-21
Reporter johan Assigned To yakobowski Resolution fixed
Priority normal Severity crash Reproducibility always
Platform - OS Linux OS Version Debian Jessie
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version Frama-C Aluminium

Description :

Running "frama-c -jessie -jessie-atp=gui" on a simpler file works, but on the attached file, it produces an ml backtrace and asks me to report it as a crash to the BTS.

Additional Information :

The -enable-journal option, which the bug reporting guidelines encourage me to use, only tells me user "error: option `-enable-journal' is unknown."

Full output: $ frama-c -jessie -jessie-atp=gui reduce.c [kernel] preprocessing with "gcc -C -E -I. -dD reduce.c" [jessie] Starting Jessie translation [kernel] Current source was: reduce.c:15 The full backtrace is: Raised at file "norm.ml", line 769, characters 52-64 Called from file "norm.ml", line 772, characters 47-69 Called from file "list.ml", line 55, characters 20-23 Called from file "norm.ml", line 788, characters 43-62 Called from file "src/kernel/visitor.ml", line 162, characters 14-30 Called from file "src/kernel/visitor.ml", line 384, characters 21-46 Called from file "list.ml", line 66, characters 22-25 Called from file "src/kernel/visitor.ml", line 382, characters 8-398 Called from file "src/kernel/visitor.ml", line 583, characters 29-45 Called from file "src/kernel/visitor.ml", line 784, characters 6-21 Called from file "cil/src/cil.ml", line 3280, characters 5-53 Called from file "cil/src/cil.ml", line 5881, characters 17-37 Called from file "cil/src/cil.ml", line 5888, characters 3-20 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 5905, characters 15-39 Called from file "norm.ml", line 1875, characters 2-27 Called from file "register.ml", line 159, characters 4-23 Called from file "register.ml", line 327, characters 6-12 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 735, characters 2-9 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8

     Unexpected error (File "norm.ml", line 769, characters 52-58: Assertion failed).
     Please report as 'crash' at http://bts.frama-c.com/.
     Your Frama-C version is Neon-20140301.
     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 :

Run "frama-c -jessie -jessie-atp=gui reduce.c" with the attached file reduce.c

Attachments

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