no conversion int[] to int* for logic fct arg; exprs a and &a[0] treated differently
ID0000841: This issue was created automatically from Mantis Issue 841. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000841 | Frama-C | Kernel > ACSL implementation | public | 2011-05-27 | 2011-10-10 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | tweak | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
In the attached program, the logic function p expects an int* argument.
When supplied the int[] argument (a), the kernel reports a user error (line 8), which is at least unfamiliar to C programmers.
Supplying the argument (&a[0]) causes no error message (line 7).