Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001906Frama-CPlug-in > slicingpublic2014-08-06 11:272014-08-06 16:14
Reporterzenscr 
Assigned Topatrick 
PriorityhighSeveritycrashReproducibilityalways
StatusclosedResolutionduplicate 
PlatformOSArch LinuxOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in Version 
Summary0001906: Crash in the case of multiple pragma statements
DescriptionIn the case of multiple pragma ctrl statements within the code to slice, the slicing plugin crashs immediately.
Steps To ReproduceUsing the attached program, execute Frama-C's slicing plugin as follows frama-c branches.c -slice-pragma branches -then-on 'Slicing export' -print
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
TagsNo tags attached.
Attached Filesc file icon branches.c [^] (2,369 bytes) 2014-08-06 11:27 [Show Content]

- Relationships
duplicate of 0001768closedpatrick Crah with the option -ulevel 

-  Notes
(0005383)
patrick (developer)
2014-08-06 16:14

This issue was the main reason of the one found previously.

- Issue History
Date Modified Username Field Change
2014-08-06 11:27 zenscr New Issue
2014-08-06 11:27 zenscr File Added: branches.c
2014-08-06 12:27 signoles Assigned To => patrick
2014-08-06 12:27 signoles Status new => assigned
2014-08-06 16:09 patrick Relationship added duplicate of 0001768
2014-08-06 16:14 patrick Note Added: 0005383
2014-08-06 16:14 patrick Status assigned => closed
2014-08-06 16:14 patrick Resolution open => duplicate


Copyright © 2000 - 2020 MantisBT Team
Powered by Mantis Bugtracker