2021-02-24 19:04 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000825Frama-CPlug-in > slicingpublic2014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • tgz file icon c.tgz (38,425 bytes) 2011-05-14 01:44

-Relationships
+Relationships

-Notes

~0001896

Anne (reporter)

[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)

Last edited: 2011-05-16 09:31

I have found why : the statement seems unreachable... but both branches are reachable through [goto] statements.

~0001898

pascal (reporter)

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)

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)

Yes : I suppose you are right. People are not supposed to write unreachable code, but it might happen...

~0004787

Anne (reporter)

Fix committed to stable/neon branch.
+Notes

-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
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
2013-12-19 01:12 Anne Source_changeset_attached => framac master 4d9cd4a1
2014-02-12 16:54 Anne Source_changeset_attached => framac stable/neon 4d9cd4a1
2014-02-12 16:59 Anne Note Added: 0004787
2014-02-12 16:59 Anne Status closed => resolved
+Issue History