GitLab

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