Frama-C Bug Tracking System - Frama-C
View Issue Details
0000825Frama-CPlug-in > slicingpublic2011-05-14 01:442014-02-12 16:59
pascal 
Anne 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000825: r13465, crash in slicing (csmith)
Command: ~/ppc/bin/toplevel.opt -val-signed-overflow-alarms s.14013538.2.c -cpp-command "gcc -m32 -I runtime -D__FRAMAC -C -E " -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode test.i ... [slicing] exporting project to 'Slicing export'... [slicing] applying all slicing requests... [slicing] applying 0 actions... [kernel] The full backtrace is: Called from file "src/misc/filter.ml", line 406, characters 13-62 Called from file "src/kernel/visitor.ml", line 155, characters 17-23 Called from file "cil/src/cil.ml", line 7395, characters 5-86 Called from file "cil/src/cil.ml", line 6481, characters 13-16 Called from file "cil/src/cil.ml", line 7529, characters 16-40 Called from file "cil/src/cil.ml", line 6458, characters 21-41 Called from file "src/misc/filter.ml", line 404, characters 25-71 Called from file "src/kernel/visitor.ml", line 155, characters 17-23 Called from file "cil/src/cil.ml", line 7395, characters 5-86 Called from file "cil/src/cil.ml", line 6481, characters 13-16 Called from file "cil/src/cil.ml", line 7529, characters 16-40 Called from file "cil/src/cil.ml", line 6458, characters 21-41 Called from file "src/misc/filter.ml", line 512, characters 21-69 Called from file "src/misc/filter.ml", line 701, characters 13-25 Called from file "list.ml", line 57, characters 20-23 Called from file "src/misc/filter.ml", line 718, characters 23-59 Called from file "src/kernel/visitor.ml", line 186, characters 14-30 Called from file "cil/src/cil.ml", line 6512, characters 15-31 Called from file "cil/src/cil.ml", line 7787, characters 5-63 Called from file "cil/src/cil.ml", line 8125, characters 17-37 Called from file "cil/src/cil.ml", line 8132, characters 3-20 Called from file "cil/src/cil.ml", line 6458, characters 21-41 Called from file "src/kernel/file.ml", line 1294, characters 14-47 Called from file "src/kernel/file.ml", line 1326, characters 2-34 Called from file "src/misc/filter.ml", line 741, characters 14-71 Called from file "src/slicing/slicingTransform.ml", line 431, characters 4-69 Called from file "src/slicing/register.ml", line 1171, characters 6-61 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 36, characters 4-20 Called from file "src/kernel/cmdline.ml", line 723, characters 2-9 Called from file "src/kernel/cmdline.ml", line 200, characters 4-8 Unexpected error (File "src/misc/filter.ml", line 204, characters 15-21: Assertion failed). Please report as 'crash' at http://bts.frama-c.com/. Your Frama-C version is Carbon-20110201+dev. Note that a version and a backtrace alone often does not have 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
No tags attached.
tgz c.tgz (38,425) 2011-05-14 01:44
https://bts.frama-c.com/file_download.php?file_id=216&type=bug
Issue History
2011-05-14 01:44pascalNew Issue
2011-05-14 01:44pascalStatusnew => assigned
2011-05-14 01:44pascalAssigned To => Anne
2011-05-14 01:44pascalFile Added: c.tgz
2011-05-14 01:45pascalSummaryr13465, crash in slicing => r13465, crash in slicing (csmith)
2011-05-16 09:05AnneNote Added: 0001896
2011-05-16 09:27AnneNote Added: 0001897
2011-05-16 09:31AnneNote Edited: 0001897
2011-05-16 10:50pascalNote Added: 0001898
2011-05-16 11:02pascalNote Added: 0001899
2011-05-16 13:30AnneNote Added: 0001900
2011-05-16 14:01svnCheckin
2011-05-16 14:01svnStatusassigned => resolved
2011-05-16 14:01svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed
2014-02-12 16:59AnneNote Added: 0004787
2014-02-12 16:59AnneStatusclosed => resolved

Notes
(0001896)
Anne   
2011-05-16 09:05   
[Db.Value.condition_truth_value] returned (false, false), and we saw that it can happen when the statement is not registered in [Db.Conditions_table]. But when does that happen more precisely ?
(0001897)
Anne   
2011-05-16 09:27   
(edited on: 2011-05-16 09:31)
I have found why : the statement seems unreachable... but both branches are reachable through [goto] statements.
(0001898)
pascal   
2011-05-16 10:50   
Another possibility is that for all paths explored by the value analysis, the evaluation of the condition ends in run-time error. The programs generated by Csmith are supposed to be well-defined but 1) I have reported several bugs where they weren't 2) the if can be unreachable in reality, and appear to be reached in the value analysis with values that make the condition produce a run-time error.
(0001899)
pascal   
2011-05-16 11:02   
Actually, generation of "gotos" was supposed to be disabled when producing this example, so the gotos would have been generated by CIL and similar situations are likely to come up again often in programs written with a lot of && and ||.
(0001900)
Anne   
2011-05-16 13:30   
Yes : I suppose you are right. People are not supposed to write unreachable code, but it might happen...
(0004787)
Anne   
2014-02-12 16:59   
Fix committed to stable/neon branch.