Alignment of global character arrays
ID0000873: This issue was created automatically from Mantis Issue 873. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000873 | Frama-C | Plug-in > Eva | public | 2011-06-28 | 2013-02-22 |
| Reporter | ddelmas | Assigned To | yakobowski | Resolution | fixed |
| Priority | normal | Severity | feature | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | - |
Description :
With the attached source file,
$ frama-c tab_char.c -val
produces the (correct) output :
[value] Called Frama_C_show_each_Alignment( {{ &"WARNING: address possibly non word aligned" ;}}, {{ &t ;}})
However, adding options -machdep ppc_32_diab does not change this output, although character arrays have a default alignment of 4 with the Diab C cross-compiler for PowerPC.
It would be useful to have -machdep ppc_32_diab take this specific feature into account.