|
Notes |
|
|
|
__builtin_va_start is indeed a built-in known by Frama-C for some machdeps, including all those currently released. The correct user-accessible declaration is
extern void __builtin_va_start(__builtin_va_list);
With this declaration, the warning disappears. Note that calls to __builtin_va_(start|arg|end) are entirely ignored by value anyway. |
|
|
|
(0003695)
|
|
Jochen
|
|
2013-02-15 11:01
|
|
|
Boris, thank you for your above note; your hints made our warnings about __builtin_va_xxx disappear. It may be sufficient to include these hints at an appropriate place in the Acsl manual. |
|
|
|
|
|
This is not really related to ACSL, but to the plugins that need a spec for the _builtin_va_ functions. An internship related to variadic C functions is ongoing. Notice that _builtin_va_start and its friends are not proper C functions wrt. the types of their arguments, so we will need to change the AST anyway. |
|
|
|
|
|
Variadic functions will be handled automatically in Frama-C Aluminium. |
|
|
|
|
|
Builtin variadic (option -va) will transform variadic functions into non-variadic ones, and add specifications when possible. I'm not fond of Changing the ACSL manual because this issue is quite Frama-C centric. |
|
ftest.c (313) 2013-02-14 14:47