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

Crash in the case of multiple pragma statements

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


Id Project Category View Due Date Updated
ID0001906 Frama-C Plug-in > slicing public 2014-08-06 2014-08-06
Reporter zenscr Assigned To patrick Resolution duplicate
Priority high Severity crash Reproducibility always
Platform - OS Arch Linux OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version -

Description :

In the case of multiple pragma ctrl statements within the code to slice, the slicing plugin crashs immediately.

Additional Information :

[kernel] preprocessing with "gcc -C -E -I. branches.c" branches1-true.c:13:[kernel] warning: Body of function branches falls-through. Adding a return statement [slicing] slicing requests in progress... [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization

[value] computing for function __VERIFIER_nondet_int <- main. Called from branches1-true.c:76. branches1-true.c:76:[kernel] warning: Neither code nor specification for function __VERIFIER_nondet_int, generating default assigns from the prototype [value] using specification for function __VERIFIER_nondet_int [value] Done for function __VERIFIER_nondet_int [value] computing for function __VERIFIER_nondet_int <- main. Called from branches1-true.c:77. [value] Done for function __VERIFIER_nondet_int [value] computing for function __VERIFIER_nondet_int <- main. Called from branches1-true.c:78. [value] Done for function __VERIFIER_nondet_int [value] computing for function __VERIFIER_nondet_int <- main. Called from branches1-true.c:79. [value] Done for function __VERIFIER_nondet_int [value] computing for function __VERIFIER_nondet_int <- main. Called from branches1-true.c:80. [value] Done for function __VERIFIER_nondet_int [value] computing for function __VERIFIER_nondet_int <- main. Called from branches1-true.c:81. [value] Done for function __VERIFIER_nondet_int [value] computing for function branches <- main. Called from branches1-true.c:90. [value] computing for function __assert_fail <- branches <- main. Called from branches1-true.c:66. branches1-true.c:66:[kernel] warning: Neither code nor specification for function __assert_fail, generating default assigns from the prototype [value] using specification for function __assert_fail [value] Done for function __assert_fail [value] computing for function __assert_fail <- branches <- main. Called from branches1-true.c:55. [value] Done for function __assert_fail [value] computing for function __assert_fail <- branches <- main. Called from branches1-true.c:59. [value] Done for function __assert_fail branches1-true.c:70:[value] Assertion got status invalid (stopping propagation). [value] Recording results for branches [value] Done for function branches [value] computing for function exit <- main. Called from branches1-true.c:93. branches1-true.c:93:[kernel] warning: Neither code nor specification for function exit, generating default assigns from the prototype [value] using specification for function exit [value] Done for function exit [value] Recording results for main [value] done for function main [slicing] making slicing project 'Slicing'... [slicing] interpreting slicing requests from the command line... [kernel] Current source was: branches.c:45 The full backtrace is: Raised at file "src/logic/logic_interp.ml", line 820, characters 6-39 Called from file "list.ml", line 73, characters 12-15 Called from file "hashtbl.ml", line 188, characters 8-13 Called from file "hashtbl.ml", line 191, characters 4-19 Called from file "src/logic/annotations.ml", line 377, characters 4-116 Called from file "src/slicing/slicingCmds.ml", line 43, characters 27-33 Called from file "cil/src/cil.ml", line 1843, characters 15-31 Called from file "cil/src/cil.ml", line 2887, characters 5-86 Called from file "cil/src/cil.ml", line 1882, characters 13-16 Called from file "cil/src/cil.ml", line 3020, characters 16-40 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2954, characters 33-42 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2887, characters 5-86 Called from file "cil/src/cil.ml", line 1882, characters 13-16 Called from file "cil/src/cil.ml", line 3020, characters 16-40 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2954, characters 11-20 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2887, characters 5-86 Called from file "cil/src/cil.ml", line 1882, characters 13-16 Called from file "cil/src/cil.ml", line 3020, characters 16-40 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2954, characters 33-42 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2887, characters 5-86 Called from file "cil/src/cil.ml", line 1882, characters 13-16 Called from file "cil/src/cil.ml", line 3020, characters 16-40 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2954, characters 11-20 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 2887, characters 5-86 Called from file "cil/src/cil.ml", line 1882, characters 13-16 Called from file "cil/src/cil.ml", line 3020, characters 16-40 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 3234, characters 14-39 Called from file "cil/src/cil.ml", line 1858, characters 21-41 Called from file "cil/src/cil.ml", line 3206, characters 5-91 Called from file "src/slicing/slicingCmds.ml", line 75, characters 11-62 Called from file "src/logic/logic_interp.ml", line 944, characters 9-44 Called from file "src/slicing/slicingCmds.ml", line 503, characters 4-260 Called from file "src/slicing/slicingCmds.ml", line 599, characters 31-64 Called from file "src/slicing/slicingCmds.ml", line 607, characters 13-274 Called from file "map.ml", line 168, characters 20-25 Called from file "map.ml", line 168, characters 10-18 Called from file "src/slicing/slicingCmds.ml", line 595, characters 6-1023 Called from file "src/slicing/register.ml", line 1194, characters 4-54 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 "src/logic/logic_interp.ml", line 820, characters 6-12: 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 :

Using the attached program, execute Frama-C's slicing plugin as follows

frama-c branches.c -slice-pragma branches -then-on 'Slicing export' -print

Attachments

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