| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000827 | Frama-C | Plug-in > slicing | public | 2011-05-18 10:39 | 2014-02-12 16:59 | ||||
| Reporter | pascal | ||||||||
| Assigned To | Anne | ||||||||
| Priority | high | 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 | 0000827: sliced program computes differently from original (csmith) | ||||||||
| Description | The commands used and results obtained are in the included testslicing.sh | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
pascal (reporter) 2011-05-18 10:48 |
I forgot to include in the archive show_each.c, the source file that is compiled into show_each-x86_32.o. Here it is: ___ #include <stdio.h> void Frama_C_show_each(unsigned int crc) { printf ("[value] Called Frama_C_show_each({%u})\n", crc); } void Frama_C_show_each_int(int c) { printf ("[value] Called Frama_C_show_each_int({%d})\n", c); } |
|
Anne (reporter) 2011-06-16 17:10 |
Here is a shorter example with the same problem : int G; int f (void) { G = 3; return 5; } int main (void) { G = f (); return G; } $ frama-c -slice-return main toto.c -slice-print gives : int G; void f_slice_1(void) { G = 3; return; } int main(void) { f_slice_1(); return (G); } In the original program, main returns 5 while in the sliced one, it returns 3. Don't know why yet :-( |
|
Anne (reporter) 2011-06-16 17:43 |
It is a PDG problem : the return output is processed before the implicit outputs. So the dependencies are mixed-up... |
|
monate (reporter) 2011-06-17 08:50 |
Merci Anne ! |
|
Anne (reporter) 2014-02-12 16:59 |
Fix committed to stable/neon branch. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-05-18 10:39 | pascal | New Issue | |
| 2011-05-18 10:39 | pascal | Status | new => assigned |
| 2011-05-18 10:39 | pascal | Assigned To | => Anne |
| 2011-05-18 10:39 | pascal | File Added: s.tgz | |
| 2011-05-18 10:48 | pascal | Note Added: 0001909 | |
| 2011-05-18 11:00 | pascal | Summary | sliced program computes differently from original => sliced program computes differently from original (csmith) |
| 2011-06-15 20:09 | monate | Priority | normal => high |
| 2011-06-16 17:10 | Anne | Note Added: 0001980 | |
| 2011-06-16 17:43 | Anne | Note Added: 0001981 | |
| 2011-06-16 17:51 | svn | ||
| 2011-06-16 17:51 | svn | Status | assigned => resolved |
| 2011-06-16 17:51 | svn | Resolution | open => fixed |
| 2011-06-17 08:50 | monate | Note Added: 0001983 | |
| 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 5c51c5dd |
| 2014-02-12 16:54 | Anne | Source_changeset_attached | => framac stable/neon 5c51c5dd |
| 2014-02-12 16:59 | Anne | Note Added: 0004772 | |
| 2014-02-12 16:59 | Anne | Status | closed => resolved |
| Issue History |