Frama-C Bug Tracking System - Frama-C
View Issue Details
0000841Frama-CKernel > ACSL implementationpublic2011-05-27 16:132011-10-10 14:14
Jochen 
virgile 
normaltweakalways
closedfixed 
Frama-C Carbon-20110201 
Frama-C Nitrogen-20111001 
0000841: no conversion int[] to int* for logic fct arg; exprs a and &a[0] treated differently
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).
No tags attached.
c ftest.c (135) 2011-05-27 16:13
https://bts.frama-c.com/file_download.php?file_id=225&type=bug
Issue History
2011-05-27 16:13JochenNew Issue
2011-05-27 16:13JochenFile Added: ftest.c
2011-05-27 16:50signolesStatusnew => assigned
2011-05-27 16:50signolesAssigned To => virgile
2011-05-27 16:50signolesCategoryKernel => Kernel > ACSL implementation
2011-06-15 20:07monateStatusassigned => acknowledged
2011-06-22 13:47virgileNote Added: 0001989
2011-06-22 14:12svnCheckin
2011-06-22 14:12svnStatusacknowledged => resolved
2011-06-22 14:12svnResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0001989)
virgile   
2011-06-22 13:47   
ACSL states specifically that a conversion from a C array to a pointer must be done explicitly (either through a cast or by taking the address of the first element). I'll change the error message to a more specific one in this case.