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