--- layout: fc_discuss_archives title: Message 11 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



Dear all,

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);

while using frama-c to handle it, the following errors emit:

"user error: expecting a non-void pointer in annotation."


How to write assigns for such kind of argument in order to specify the
side effect of function f?

I can't find any related content in the ACSL document.

Any suggestion is welcomed . Thanks.

All the best.

-david