--- layout: fc_discuss_archives title: Message 12 from Frama-C-discuss on December 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to write assign for void* type argument of a function



On Sun, Dec 8, 2013 at 4:54 PM, David Yang <abiao.yang at gmail.com> wrote:

>
> While there has a void pointer argument in function, I found I could
> not write assign for these arguments.
>
> e.g.
>
> /*@ assigns *data; */
> int f(void * data);
>
>
Well, void is an ?incomplete type?. C does not let you dereference a
pointer to void either: as an incomplete type, void has no size so the C
compiler would not know what to read.

Use:

 assigns *((int *)data);

or anything that is appropriate to your case.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131208/319e7cfb/attachment.html>