17517: defined program behaves differently after going through -print (csmith)
ID0001115: This issue was created automatically from Mantis Issue 1115. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001115 | Frama-C | Kernel | public | 2012-03-10 | 2012-03-11 |
| Reporter | pascal | Assigned To | - | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
Program o.i is defined for a x86_64 architecture according to: $ ~/ppc/bin/toplevel.opt -val -obviously-terminates o.i -machdep x86_64 -no-val-show-progress -unspecified-access -val-signed-overflow-alarms -no-collapse-call-cast
Compiling and executing o.i:
$ gcc o.i show_each.c -o o t3.c: In function ‘func_31’: t3.c:281: warning: large integer implicitly truncated to unsigned type t3.c:299: warning: comparison of distinct pointer types lacks a cast $ ./o ... [value] Called Frama_C_show_each({3203885237})
However, parsing and printing o.i into t.i yields a program that computes differently when compiled: $ ~/ppc/bin/toplevel.opt -machdep x86_64 o.i -print > t.i $ gcc t.i show_each.c -o t $ ./t ... [value] Called Frama_C_show_each({4108310006})