Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000858Frama-CPlug-in > semantic constant foldingpublic2011-06-08 14:122014-02-12 16:59
Reporterpascal 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000858: emitted program computes differently from original (csmith)
Descriptioncuoq@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})
TagsNo tags attached.
Attached Filestgz file icon scf858.tgz [^] (38,635 bytes) 2011-06-08 14:12

- Relationships

-  Notes
(0001960)
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.
(0001961)
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)
(0004773)
monate (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- 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 Checkin
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
2014-02-12 16:59 monate Note Added: 0004773
2014-02-12 16:59 monate Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker