Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>