Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000825Frama-CPlug-in > slicingpublic2011-05-14 01:442014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000825: r13465, crash in slicing (csmith)
DescriptionCommand: ~/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 [^]
TagsNo tags attached.
Attached Filestgz file icon c.tgz [^] (38,425 bytes) 2011-05-14 01:44

- Relationships

-  Notes
(0001896)
Anne (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-05-14 01:44 pascal New Issue
2011-05-14 01:44 pascal Status new => assigned
2011-05-14 01:44 pascal Assigned To => Anne
2011-05-14 01:44 pascal File Added: c.tgz
2011-05-14 01:45 pascal Summary r13465, crash in slicing => r13465, crash in slicing (csmith)
2011-05-16 09:05 Anne Note Added: 0001896
2011-05-16 09:27 Anne Note Added: 0001897
2011-05-16 09:31 Anne Note Edited: 0001897
2011-05-16 10:50 pascal Note Added: 0001898
2011-05-16 11:02 pascal Note Added: 0001899
2011-05-16 13:30 Anne Note Added: 0001900
2011-05-16 14:01 svn Checkin
2011-05-16 14:01 svn Status assigned => resolved
2011-05-16 14:01 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2014-02-12 16:59 Anne Note Added: 0004787
2014-02-12 16:59 Anne Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker