Frama-C Bug Tracking System - Frama-C |
| View Issue Details |
|
| 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 | |
| Platform | | OS | | OS Version | |
| 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
|
| Steps To Reproduce | |
| Additional Information | |
| Tags | No tags attached. |
| Relationships | |
| Attached Files |  s.tgz (63,223) 2011-05-18 10:39
https://bts.frama-c.com/file_download.php?file_id=218&type=bug |
|
| 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 | Checkin | |
| 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 |
| 2014-02-12 16:59 | Anne | Note Added: 0004772 | |
| 2014-02-12 16:59 | Anne | Status | closed => resolved |
|
Notes |
|
|
(0001909)
|
|
pascal
|
|
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
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);
} |
|
|
|
(0001980)
|
|
Anne
|
|
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 :-( |
|
|
|
(0001981)
|
|
Anne
|
|
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... |
|
|
|
(0001983)
|
|
monate
|
|
2011-06-17 08:50
|
|
|
|
|
(0004772)
|
|
Anne
|
|
2014-02-12 16:59
|
|
|
Fix committed to stable/neon branch. |
|