2020-12-05 00:08 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000858Frama-CPlug-in > semantic constant foldingpublic2014-02-12 16:59
Reporterpascal 
Assigned Tomonate 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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 Files

-Relationships
+Relationships

-Notes

~0001960

pascal (reporter)

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)

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)

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