| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000825 | Frama-C | Plug-in > slicing | public | 2011-05-14 01:44 | 2014-02-12 16:59 | ||||
| Reporter | pascal | ||||||||
| Assigned To | Anne | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000825: r13465, crash in slicing (csmith) | ||||||||
| Description | 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 | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
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 ? |
|
Anne (reporter) 2011-05-16 09:27 Last edited: 2011-05-16 09:31 |
I have found why : the statement seems unreachable... but both branches are reachable through [goto] statements. |
|
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. |
|
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 ||. |
|
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... |
|
Anne (reporter) 2014-02-12 16:59 |
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 |