| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
|---|---|---|---|---|---|---|---|---|---|
| 0000858 | Frama-C | Plug-in > semantic constant folding | public | 2011-06-08 14:12 | 2014-02-12 16:59 | ||||
| Reporter | pascal | ||||||||
| Assigned To | monate | ||||||||
| Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
| Status | closed | Resolution | fixed | ||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000858: emitted program computes differently from original (csmith) | ||||||||
| Description | cuoq@ns61143:~/csmith$ cat scf.08000752.exec [value] Called Frama_C_show_each({8413297}) [value] Called Frama_C_show_each({3974178539}) [value] Called Frama_C_show_each({3974178539}) cuoq@ns61143:~/csmith$ ~/ppc/bin/toplevel.opt -val -cpp-command "gcc -C -E -I $CSMITH/runtime -D__FRAMAC " -slevel 50 -no-results-function crc32_gentab -semantic-const-folding -quiet -machdep x86_64 scf.08000752.c | ./selin.pl > scf.i cuoq@ns61143:~/csmith$ gcc scf.i show_each-x86_64.o cuoq@ns61143:~/csmith$ ./a.out [value] Called Frama_C_show_each({8413297}) [value] Called Frama_C_show_each({844760584}) [value] Called Frama_C_show_each({844760584}) | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |
| ||||||||
 Relationships |
|
 Relationships |
| Notes |
|
|
pascal (reporter) 2011-06-08 14:21 |
Additional command: the .exec file was made from: ~/t $ gcc -Iruntime -D__FRAMAC scf.08000752.c show_each.c ~/t $ ./a.out [value] Called Frama_C_show_each({8413297}) [value] Called Frama_C_show_each({3974178539}) [value] Called Frama_C_show_each({3974178539}) This seems like a machdep issue: the sliced program compiled as 32-bit produces the expected result. It's only compiled as 64-bit that it produces There were changes related to machdep and projects recently, I need to get more information about that. Perhaps this bug is already fixed in the latest SVN. |
|
pascal (reporter) 2011-06-08 14:33 |
Produced again with clean SVN checkout on lsl-cloud.com, OCaml 3.12.0 64-bit. The bug is sensitive to system headers: better reproduce it there. cuoq@ns61143:~/csmith$ ~/svn_ppc/bin/toplevel.opt -val -cpp-command "gcc -C -E -I $CSMITH/runtime -D__FRAMAC " -slevel 50 -no-results-function crc32_gentab -semantic-const-folding -quiet -machdep x86_64 scf.08000752.c | ./selin.pl > scf.i cuoq@ns61143:~/csmith$ gcc -Iruntime -D__FRAMAC scf.08000752.c show_each.c cuoq@ns61143:~/csmith$ ./a.out [value] Called Frama_C_show_each({8413297}) [value] Called Frama_C_show_each({3974178539}) [value] Called Frama_C_show_each({3974178539}) cuoq@ns61143:~/csmith$ gcc -Iruntime -D__FRAMAC scf.i show_each.c cuoq@ns61143:~/csmith$ ./a.out [value] Called Frama_C_show_each({8413297}) [value] Called Frama_C_show_each({844760584}) [value] Called Frama_C_show_each({844760584}) cuoq@ns61143:~/csmith$ svn info ~/svn_ppc/ Path: /home/cuoq/svn_ppc URL: https://svn.frama-c.com/frama-c/trunk Repository Root: https://svn.frama-c.com/frama-c Repository UUID: 144eed1f-067f-4a55-9ecd-662404a24857 Revision: 13868 Node Kind: directory Schedule: normal Last Changed Author: correnson Last Changed Rev: 13863 Last Changed Date: 2011-06-08 12:30:52 +0200 (Wed, 08 Jun 2011) |
|
monate (reporter) 2014-02-12 16:59 |
Fix committed to stable/neon branch. |
| Notes |
| Issue History |
|||
| Date Modified | Username | Field | Change |
|---|---|---|---|
| 2011-06-08 14:12 | pascal | New Issue | |
| 2011-06-08 14:12 | pascal | Status | new => assigned |
| 2011-06-08 14:12 | pascal | Assigned To | => monate |
| 2011-06-08 14:12 | pascal | File Added: scf858.tgz | |
| 2011-06-08 14:13 | pascal | Product Version | => Frama-C GIT, precise the release id |
| 2011-06-08 14:13 | pascal | Summary | emitted program computes differently from original => emitted program computes differently from original (csmith) |
| 2011-06-08 14:21 | pascal | Note Added: 0001960 | |
| 2011-06-08 14:33 | pascal | Note Added: 0001961 | |
| 2011-06-14 15:38 | svn | ||
| 2011-06-14 15:38 | svn | Status | assigned => resolved |
| 2011-06-14 15:38 | 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 |
| 2011-12-18 21:41 | pascal | Status | closed => feedback |
| 2011-12-18 21:41 | pascal | Resolution | fixed => reopened |
| 2011-12-18 21:41 | pascal | View Status | private => public |
| 2011-12-18 21:43 | pascal | Status | feedback => closed |
| 2011-12-18 21:43 | pascal | Resolution | reopened => fixed |
| 2013-12-19 01:12 | svn | Source_changeset_attached | => framac master 3386e2bc |
| 2014-02-12 16:54 | monate | Source_changeset_attached | => framac stable/neon 3386e2bc |
| 2014-02-12 16:59 | monate | Note Added: 0004773 | |
| 2014-02-12 16:59 | monate | Status | closed => resolved |
| Issue History |