| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000802 | Frama-C | Plug-in > slicing | public | 2011-04-20 16:33 | 2011-10-10 14:14 | ||||
| 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 | 0000802: r12951, sliced program does not terminate | ||||||||
| Description | The original program terminates: gcc -I runtime -m32 show_each.c nonterminatingslice/s.20153409.4.c ./a.out [value] Called Frama_C_show_each({1696784233; }) [value] Called Frama_C_show_each({538004427; }) [value] Called Frama_C_show_each({3729539076; }) [value] Called Frama_C_show_each({3984566477; }) [value] Called Frama_C_show_each({2563812225; }) [value] Called Frama_C_show_each({1179156549; }) [value] Called Frama_C_show_each({1179156549; }) The sliced one doesn't. The slicing command was: ~/ppc/bin/toplevel.opt -val-signed-overflow-alarms nonterminatingslice/s.20153409.4.c -cpp-command "gcc -m32 -C -E -D__FRAMAC -I. -I$CSMITH/runtime " -slice-calls Frama_C_show_each -slevel 5000 -slevel-function crc32_gentab:0 -then-on 'Slicing export' -print -ocode s.c | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
||||||
|
||||||
 Relationships |
| Notes |
|
|
Anne (reporter) 2011-04-21 10:11 |
In 0000787, we have seen that there is a problem with unreachable control statement. I thought that it could happen only if we use the value analysis results, but unfortunately, it seems that it can also happen in other cases such as this one: int g_4; void main(void) { while (1) { g_4 = 6; while (1) { return ; return ; // <--- problem here } } } frama-c -slice-value g_4 toto.c -slice-print /* Generated by Frama-C */ int g_4 ; void main(void) { while (1) { g_4 = (int )6L; while (1) { } // <-- infinite loop } return; } This doesn't happen when the second [return] is removed from the example... Don't know yet how to fix that, but have to find out ! |
|
pascal (reporter) 2011-04-21 10:19 |
Would the alternative solution to 787 (postdominator analysis that takes into account unreachable statements) fix this as well? |
|
Anne (reporter) 2011-04-21 13:20 |
Yes : I think so. But I am wondering if it wouldn't be easier to have another tool to remove the dead code, optionally using the value analysis results... What do you think ? |
|
Anne (reporter) 2011-04-28 13:58 |
Fixed in rev 13064. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-04-20 16:33 | pascal | New Issue | |
| 2011-04-20 16:33 | pascal | Status | new => assigned |
| 2011-04-20 16:33 | pascal | Assigned To | => Anne |
| 2011-04-20 18:11 | pascal | File Added: nt.tgz | |
| 2011-04-21 09:09 | Anne | Relationship added | related to 0000787 |
| 2011-04-21 10:11 | Anne | Note Added: 0001802 | |
| 2011-04-21 10:19 | pascal | Note Added: 0001803 | |
| 2011-04-21 13:20 | Anne | Note Added: 0001805 | |
| 2011-04-28 13:58 | Anne | Note Added: 0001817 | |
| 2011-04-28 13:58 | Anne | Status | assigned => resolved |
| 2011-04-28 13:58 | Anne | 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 |
| Issue History |