Anonymous | Login | Signup for a new account | 2019-12-06 14:07 CET | ![]() |
Main | My View | View Issues | Change Log | Roadmap | Repositories |
View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ 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 | ||||||
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 | ||||||||
Tags | No tags attached. | ||||||||
Attached Files | ![]() | ||||||||
![]() |
|
(0001909) 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 |
(0001980) 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 :-( |
(0001981) 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... |
(0001983) monate (reporter) 2011-06-17 08:50 |
Merci Anne ! |
(0004772) Anne (reporter) 2014-02-12 16:59 |
Fix committed to stable/neon branch. |
![]() |
|||
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 |
Copyright © 2000 - 2019 MantisBT Team |