0000858: emitted program computes differently from original (csmith)

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

Relationships