Sliced program computes differently from original (csmith)
ID0000963: This issue was created automatically from Mantis Issue 963. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000963 | Frama-C | Plug-in > slicing | public | 2011-09-14 | 2014-02-12 |
| Reporter | pascal | Assigned To | Anne | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
Bon, j'ai peut-être un peu perdu la main, alors il faudra m'excuser si je rapporte un non-problème, ou si j'oublie des détails au début.
L'architecture cible est maintenant -machdep x86_64 (on a maintenant confiance dans l'analyse de valeurs sur cette architecture).
La commande de slicing utilisée est dans le script slice_src_dest.sh
Pour compiler l'original ou le programme slicé:
gcc -Iruntime s.14134425.9.c show_each.c -o orig gcc -Iruntime s.14134425.9.s.c show_each.c -o slice
(c'est un gcc 64-bit)
J'obtiens les fichiers .exec et .execs, qui sont différents.